0 Prolog
↳1 PrologToDTProblemTransformerProof (⇒, 289 ms)
↳2 TRIPLES
↳3 TriplesToPiDPProof (⇒, 512 ms)
↳4 PiDP
↳5 DependencyGraphProof (⇔, 0 ms)
↳6 AND
↳7 PiDP
↳8 UsableRulesProof (⇔, 0 ms)
↳9 PiDP
↳10 PiDPToQDPProof (⇔, 16 ms)
↳11 QDP
↳12 QDPSizeChangeProof (⇔, 0 ms)
↳13 YES
↳14 PiDP
↳15 UsableRulesProof (⇔, 0 ms)
↳16 PiDP
↳17 PiDPToQDPProof (⇔, 0 ms)
↳18 QDP
↳19 QDPSizeChangeProof (⇔, 0 ms)
↳20 YES
↳21 PiDP
↳22 UsableRulesProof (⇔, 0 ms)
↳23 PiDP
↳24 PiDPToQDPProof (⇒, 0 ms)
↳25 QDP
↳26 QDPSizeChangeProof (⇔, 0 ms)
↳27 YES
↳28 PiDP
↳29 UsableRulesProof (⇔, 0 ms)
↳30 PiDP
↳31 PiDPToQDPProof (⇒, 0 ms)
↳32 QDP
↳33 QDPSizeChangeProof (⇔, 0 ms)
↳34 YES
↳35 PiDP
↳36 UsableRulesProof (⇔, 0 ms)
↳37 PiDP
↳38 PiDPToQDPProof (⇒, 40 ms)
↳39 QDP
↳40 Rewriting (⇔, 149 ms)
↳41 QDP
↳42 Rewriting (⇔, 0 ms)
↳43 QDP
↳44 QDPOrderProof (⇔, 1831 ms)
↳45 QDP
↳46 DependencyGraphProof (⇔, 0 ms)
↳47 TRUE
↳48 PiDP
↳49 UsableRulesProof (⇔, 0 ms)
↳50 PiDP
↳51 PiDPToQDPProof (⇒, 0 ms)
↳52 QDP
↳53 Rewriting (⇔, 0 ms)
↳54 QDP
↳55 UsableRulesProof (⇔, 0 ms)
↳56 QDP
↳57 QReductionProof (⇔, 0 ms)
↳58 QDP
↳59 QDPOrderProof (⇔, 27 ms)
↳60 QDP
↳61 DependencyGraphProof (⇔, 0 ms)
↳62 TRUE
MERGESORTB_IN_GAA(.(X1, .(X2, X3)), X4, .(X5, X6)) → U24_GAA(X1, X2, X3, X4, X5, X6, splitD_in_ggaaa(X2, X3, X7, X8, X6))
MERGESORTB_IN_GAA(.(X1, .(X2, X3)), X4, .(X5, X6)) → SPLITD_IN_GGAAA(X2, X3, X7, X8, X6)
SPLITD_IN_GGAAA(X1, X2, .(X1, X3), X4, .(X5, X6)) → U2_GGAAA(X1, X2, X3, X4, X5, X6, splitA_in_gaaa(X2, X4, X3, X6))
SPLITD_IN_GGAAA(X1, X2, .(X1, X3), X4, .(X5, X6)) → SPLITA_IN_GAAA(X2, X4, X3, X6)
SPLITA_IN_GAAA(.(X1, X2), .(X1, X3), X4, .(X5, X6)) → U1_GAAA(X1, X2, X3, X4, X5, X6, splitA_in_gaaa(X2, X4, X3, X6))
SPLITA_IN_GAAA(.(X1, X2), .(X1, X3), X4, .(X5, X6)) → SPLITA_IN_GAAA(X2, X4, X3, X6)
MERGESORTB_IN_GAA(.(X1, .(X2, X3)), X4, .(X5, X6)) → U25_GAA(X1, X2, X3, X4, X5, X6, splitcD_in_ggaaa(X2, X3, X7, X8, X6))
U25_GAA(X1, X2, X3, X4, X5, X6, splitcD_out_ggaaa(X2, X3, X7, X8, X6)) → U26_GAA(X1, X2, X3, X4, X5, X6, mergesortB_in_gaa(.(X1, X8), X9, X6))
U25_GAA(X1, X2, X3, X4, X5, X6, splitcD_out_ggaaa(X2, X3, X7, X8, X6)) → MERGESORTB_IN_GAA(.(X1, X8), X9, X6)
U25_GAA(X1, X2, X3, X4, X5, X6, splitcD_out_ggaaa(X2, X3, X7, X8, X6)) → U27_GAA(X1, X2, X3, X4, X5, X6, X7, mergesortcB_in_gaa(.(X1, X8), X9, X6))
U27_GAA(X1, X2, X3, X4, X5, X6, X7, mergesortcB_out_gaa(.(X1, X8), X9, X6)) → U28_GAA(X1, X2, X3, X4, X5, X6, mergesortE_in_gaa(X7, X10, X6))
U27_GAA(X1, X2, X3, X4, X5, X6, X7, mergesortcB_out_gaa(.(X1, X8), X9, X6)) → MERGESORTE_IN_GAA(X7, X10, X6)
MERGESORTE_IN_GAA(.(X1, .(X2, X3)), X4, .(X5, X6)) → U3_GAA(X1, X2, X3, X4, X5, X6, splitD_in_ggaaa(X1, .(X2, X3), X7, X8, .(X5, X6)))
MERGESORTE_IN_GAA(.(X1, .(X2, X3)), X4, .(X5, X6)) → SPLITD_IN_GGAAA(X1, .(X2, X3), X7, X8, .(X5, X6))
MERGESORTE_IN_GAA(.(X1, .(X2, X3)), X4, .(X5, X6)) → U4_GAA(X1, X2, X3, X4, X5, X6, splitcD_in_ggaaa(X1, .(X2, X3), X7, X8, .(X5, X6)))
U4_GAA(X1, X2, X3, X4, X5, X6, splitcD_out_ggaaa(X1, .(X2, X3), X7, X8, .(X5, X6))) → U5_GAA(X1, X2, X3, X4, X5, X6, mergesortE_in_gaa(X7, X9, X6))
U4_GAA(X1, X2, X3, X4, X5, X6, splitcD_out_ggaaa(X1, .(X2, X3), X7, X8, .(X5, X6))) → MERGESORTE_IN_GAA(X7, X9, X6)
U4_GAA(X1, X2, X3, X4, X5, X6, splitcD_out_ggaaa(X1, .(X2, X3), X7, X8, .(X5, X6))) → U6_GAA(X1, X2, X3, X4, X5, X6, X8, mergesortcE_in_gaa(X7, X9, X6))
U6_GAA(X1, X2, X3, X4, X5, X6, X8, mergesortcE_out_gaa(X7, X9, X6)) → U7_GAA(X1, X2, X3, X4, X5, X6, mergesortE_in_gaa(X8, X10, X6))
U6_GAA(X1, X2, X3, X4, X5, X6, X8, mergesortcE_out_gaa(X7, X9, X6)) → MERGESORTE_IN_GAA(X8, X10, X6)
U6_GAA(X1, X2, X3, X4, X5, X6, X8, mergesortcE_out_gaa(X7, X9, X6)) → U8_GAA(X1, X2, X3, X4, X5, X6, X9, mergesortcE_in_gaa(X8, X10, X6))
U8_GAA(X1, X2, X3, X4, X5, X6, X9, mergesortcE_out_gaa(X8, X10, X6)) → U9_GAA(X1, X2, X3, X4, X5, X6, mergeC_in_ggaaa(X9, X10, X4, X5, X6))
U8_GAA(X1, X2, X3, X4, X5, X6, X9, mergesortcE_out_gaa(X8, X10, X6)) → MERGEC_IN_GGAAA(X9, X10, X4, X5, X6)
MERGEC_IN_GGAAA(.(X1, X2), .(X3, X4), .(X1, X5), X6, X7) → U10_GGAAA(X1, X2, X3, X4, X5, X6, X7, pF_in_ggggaa(X1, X3, X2, X4, X5, X7))
MERGEC_IN_GGAAA(.(X1, X2), .(X3, X4), .(X1, X5), X6, X7) → PF_IN_GGGGAA(X1, X3, X2, X4, X5, X7)
PF_IN_GGGGAA(X1, X2, X3, X4, X5, X6) → U13_GGGGAA(X1, X2, X3, X4, X5, X6, leH_in_gg(X1, X2))
PF_IN_GGGGAA(X1, X2, X3, X4, X5, X6) → LEH_IN_GG(X1, X2)
LEH_IN_GG(s(X1), s(X2)) → U12_GG(X1, X2, leH_in_gg(X1, X2))
LEH_IN_GG(s(X1), s(X2)) → LEH_IN_GG(X1, X2)
PF_IN_GGGGAA(X1, X2, .(X3, X4), X5, .(X3, X6), .(X7, X8)) → U14_GGGGAA(X1, X2, X3, X4, X5, X6, X7, X8, lecH_in_gg(X1, X2))
U14_GGGGAA(X1, X2, X3, X4, X5, X6, X7, X8, lecH_out_gg(X1, X2)) → U15_GGGGAA(X1, X2, X3, X4, X5, X6, X7, X8, pF_in_ggggaa(X3, X2, X4, X5, X6, X8))
U14_GGGGAA(X1, X2, X3, X4, X5, X6, X7, X8, lecH_out_gg(X1, X2)) → PF_IN_GGGGAA(X3, X2, X4, X5, X6, X8)
PF_IN_GGGGAA(X1, X2, .(X3, X4), X5, .(X2, X6), .(X7, X8)) → U16_GGGGAA(X1, X2, X3, X4, X5, X6, X7, X8, lecH_in_gg(X1, X2))
U16_GGGGAA(X1, X2, X3, X4, X5, X6, X7, X8, lecH_out_gg(X1, X2)) → U17_GGGGAA(X1, X2, X3, X4, X5, X6, X7, X8, pG_in_ggggaa(X3, X2, X4, X5, X6, X8))
U16_GGGGAA(X1, X2, X3, X4, X5, X6, X7, X8, lecH_out_gg(X1, X2)) → PG_IN_GGGGAA(X3, X2, X4, X5, X6, X8)
PG_IN_GGGGAA(X1, X2, X3, X4, X5, X6) → U19_GGGGAA(X1, X2, X3, X4, X5, X6, gtI_in_gg(X1, X2))
PG_IN_GGGGAA(X1, X2, X3, X4, X5, X6) → GTI_IN_GG(X1, X2)
GTI_IN_GG(s(X1), s(X2)) → U18_GG(X1, X2, gtI_in_gg(X1, X2))
GTI_IN_GG(s(X1), s(X2)) → GTI_IN_GG(X1, X2)
PG_IN_GGGGAA(X1, X2, X3, .(X4, X5), .(X1, X6), .(X7, X8)) → U20_GGGGAA(X1, X2, X3, X4, X5, X6, X7, X8, gtcI_in_gg(X1, X2))
U20_GGGGAA(X1, X2, X3, X4, X5, X6, X7, X8, gtcI_out_gg(X1, X2)) → U21_GGGGAA(X1, X2, X3, X4, X5, X6, X7, X8, pF_in_ggggaa(X1, X4, X3, X5, X6, X8))
U20_GGGGAA(X1, X2, X3, X4, X5, X6, X7, X8, gtcI_out_gg(X1, X2)) → PF_IN_GGGGAA(X1, X4, X3, X5, X6, X8)
PG_IN_GGGGAA(X1, X2, X3, .(X4, X5), .(X4, X6), .(X7, X8)) → U22_GGGGAA(X1, X2, X3, X4, X5, X6, X7, X8, gtcI_in_gg(X1, X2))
U22_GGGGAA(X1, X2, X3, X4, X5, X6, X7, X8, gtcI_out_gg(X1, X2)) → U23_GGGGAA(X1, X2, X3, X4, X5, X6, X7, X8, pG_in_ggggaa(X1, X4, X3, X5, X6, X8))
U22_GGGGAA(X1, X2, X3, X4, X5, X6, X7, X8, gtcI_out_gg(X1, X2)) → PG_IN_GGGGAA(X1, X4, X3, X5, X6, X8)
MERGEC_IN_GGAAA(.(X1, X2), .(X3, X4), .(X3, X5), X6, X7) → U11_GGAAA(X1, X2, X3, X4, X5, X6, X7, pG_in_ggggaa(X1, X3, X2, X4, X5, X7))
MERGEC_IN_GGAAA(.(X1, X2), .(X3, X4), .(X3, X5), X6, X7) → PG_IN_GGGGAA(X1, X3, X2, X4, X5, X7)
U27_GAA(X1, X2, X3, X4, X5, X6, X7, mergesortcB_out_gaa(.(X1, X8), X9, X6)) → U29_GAA(X1, X2, X3, X4, X5, X6, X9, mergesortcE_in_gaa(X7, X10, X6))
U29_GAA(X1, X2, X3, X4, X5, X6, X9, mergesortcE_out_gaa(X7, X10, X6)) → U30_GAA(X1, X2, X3, X4, X5, X6, mergeC_in_ggaaa(X9, X10, X4, X5, X6))
U29_GAA(X1, X2, X3, X4, X5, X6, X9, mergesortcE_out_gaa(X7, X10, X6)) → MERGEC_IN_GGAAA(X9, X10, X4, X5, X6)
splitcD_in_ggaaa(X1, X2, .(X1, X3), X4, .(X5, X6)) → U37_ggaaa(X1, X2, X3, X4, X5, X6, splitcA_in_gaaa(X2, X4, X3, X6))
splitcA_in_gaaa([], [], [], X1) → splitcA_out_gaaa([], [], [], X1)
splitcA_in_gaaa(.(X1, X2), .(X1, X3), X4, .(X5, X6)) → U32_gaaa(X1, X2, X3, X4, X5, X6, splitcA_in_gaaa(X2, X4, X3, X6))
U32_gaaa(X1, X2, X3, X4, X5, X6, splitcA_out_gaaa(X2, X4, X3, X6)) → splitcA_out_gaaa(.(X1, X2), .(X1, X3), X4, .(X5, X6))
U37_ggaaa(X1, X2, X3, X4, X5, X6, splitcA_out_gaaa(X2, X4, X3, X6)) → splitcD_out_ggaaa(X1, X2, .(X1, X3), X4, .(X5, X6))
mergesortcB_in_gaa([], [], X1) → mergesortcB_out_gaa([], [], X1)
mergesortcB_in_gaa(.(X1, []), .(X1, []), X2) → mergesortcB_out_gaa(.(X1, []), .(X1, []), X2)
mergesortcB_in_gaa(.(X1, .(X2, X3)), X4, .(X5, X6)) → U33_gaa(X1, X2, X3, X4, X5, X6, splitcD_in_ggaaa(X2, X3, X7, X8, X6))
U33_gaa(X1, X2, X3, X4, X5, X6, splitcD_out_ggaaa(X2, X3, X7, X8, X6)) → U34_gaa(X1, X2, X3, X4, X5, X6, X7, mergesortcB_in_gaa(.(X1, X8), X9, X6))
U34_gaa(X1, X2, X3, X4, X5, X6, X7, mergesortcB_out_gaa(.(X1, X8), X9, X6)) → U35_gaa(X1, X2, X3, X4, X5, X6, X9, mergesortcE_in_gaa(X7, X10, X6))
mergesortcE_in_gaa([], [], X1) → mergesortcE_out_gaa([], [], X1)
mergesortcE_in_gaa(.(X1, []), .(X1, []), X2) → mergesortcE_out_gaa(.(X1, []), .(X1, []), X2)
mergesortcE_in_gaa(.(X1, .(X2, X3)), X4, .(X5, X6)) → U38_gaa(X1, X2, X3, X4, X5, X6, splitcD_in_ggaaa(X1, .(X2, X3), X7, X8, .(X5, X6)))
U38_gaa(X1, X2, X3, X4, X5, X6, splitcD_out_ggaaa(X1, .(X2, X3), X7, X8, .(X5, X6))) → U39_gaa(X1, X2, X3, X4, X5, X6, X8, mergesortcE_in_gaa(X7, X9, X6))
U39_gaa(X1, X2, X3, X4, X5, X6, X8, mergesortcE_out_gaa(X7, X9, X6)) → U40_gaa(X1, X2, X3, X4, X5, X6, X9, mergesortcE_in_gaa(X8, X10, X6))
U40_gaa(X1, X2, X3, X4, X5, X6, X9, mergesortcE_out_gaa(X8, X10, X6)) → U41_gaa(X1, X2, X3, X4, X5, X6, mergecC_in_ggaaa(X9, X10, X4, X5, X6))
mergecC_in_ggaaa([], X1, X1, X2, X3) → mergecC_out_ggaaa([], X1, X1, X2, X3)
mergecC_in_ggaaa(X1, [], X1, X2, X3) → mergecC_out_ggaaa(X1, [], X1, X2, X3)
mergecC_in_ggaaa(.(X1, X2), .(X3, X4), .(X1, X5), X6, X7) → U42_ggaaa(X1, X2, X3, X4, X5, X6, X7, qcF_in_ggggaa(X1, X3, X2, X4, X5, X7))
qcF_in_ggggaa(X1, X2, [], X3, .(X2, X3), X4) → U45_ggggaa(X1, X2, X3, X4, lecH_in_gg(X1, X2))
lecH_in_gg(s(X1), s(X2)) → U44_gg(X1, X2, lecH_in_gg(X1, X2))
lecH_in_gg(0, s(0)) → lecH_out_gg(0, s(0))
lecH_in_gg(0, 0) → lecH_out_gg(0, 0)
U44_gg(X1, X2, lecH_out_gg(X1, X2)) → lecH_out_gg(s(X1), s(X2))
U45_ggggaa(X1, X2, X3, X4, lecH_out_gg(X1, X2)) → qcF_out_ggggaa(X1, X2, [], X3, .(X2, X3), X4)
qcF_in_ggggaa(X1, X2, .(X3, X4), X5, .(X3, X6), .(X7, X8)) → U46_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, lecH_in_gg(X1, X2))
U46_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, lecH_out_gg(X1, X2)) → U47_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, qcF_in_ggggaa(X3, X2, X4, X5, X6, X8))
qcF_in_ggggaa(X1, X2, .(X3, X4), X5, .(X2, X6), .(X7, X8)) → U48_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, lecH_in_gg(X1, X2))
U48_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, lecH_out_gg(X1, X2)) → U49_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, qcG_in_ggggaa(X3, X2, X4, X5, X6, X8))
qcG_in_ggggaa(X1, X2, X3, [], .(X1, X3), X4) → U51_ggggaa(X1, X2, X3, X4, gtcI_in_gg(X1, X2))
gtcI_in_gg(s(X1), s(X2)) → U50_gg(X1, X2, gtcI_in_gg(X1, X2))
gtcI_in_gg(s(0), 0) → gtcI_out_gg(s(0), 0)
U50_gg(X1, X2, gtcI_out_gg(X1, X2)) → gtcI_out_gg(s(X1), s(X2))
U51_ggggaa(X1, X2, X3, X4, gtcI_out_gg(X1, X2)) → qcG_out_ggggaa(X1, X2, X3, [], .(X1, X3), X4)
qcG_in_ggggaa(X1, X2, X3, .(X4, X5), .(X1, X6), .(X7, X8)) → U52_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, gtcI_in_gg(X1, X2))
U52_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, gtcI_out_gg(X1, X2)) → U53_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, qcF_in_ggggaa(X1, X4, X3, X5, X6, X8))
U53_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, qcF_out_ggggaa(X1, X4, X3, X5, X6, X8)) → qcG_out_ggggaa(X1, X2, X3, .(X4, X5), .(X1, X6), .(X7, X8))
qcG_in_ggggaa(X1, X2, X3, .(X4, X5), .(X4, X6), .(X7, X8)) → U54_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, gtcI_in_gg(X1, X2))
U54_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, gtcI_out_gg(X1, X2)) → U55_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, qcG_in_ggggaa(X1, X4, X3, X5, X6, X8))
U55_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, qcG_out_ggggaa(X1, X4, X3, X5, X6, X8)) → qcG_out_ggggaa(X1, X2, X3, .(X4, X5), .(X4, X6), .(X7, X8))
U49_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, qcG_out_ggggaa(X3, X2, X4, X5, X6, X8)) → qcF_out_ggggaa(X1, X2, .(X3, X4), X5, .(X2, X6), .(X7, X8))
U47_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, qcF_out_ggggaa(X3, X2, X4, X5, X6, X8)) → qcF_out_ggggaa(X1, X2, .(X3, X4), X5, .(X3, X6), .(X7, X8))
U42_ggaaa(X1, X2, X3, X4, X5, X6, X7, qcF_out_ggggaa(X1, X3, X2, X4, X5, X7)) → mergecC_out_ggaaa(.(X1, X2), .(X3, X4), .(X1, X5), X6, X7)
mergecC_in_ggaaa(.(X1, X2), .(X3, X4), .(X3, X5), X6, X7) → U43_ggaaa(X1, X2, X3, X4, X5, X6, X7, qcG_in_ggggaa(X1, X3, X2, X4, X5, X7))
U43_ggaaa(X1, X2, X3, X4, X5, X6, X7, qcG_out_ggggaa(X1, X3, X2, X4, X5, X7)) → mergecC_out_ggaaa(.(X1, X2), .(X3, X4), .(X3, X5), X6, X7)
U41_gaa(X1, X2, X3, X4, X5, X6, mergecC_out_ggaaa(X9, X10, X4, X5, X6)) → mergesortcE_out_gaa(.(X1, .(X2, X3)), X4, .(X5, X6))
U35_gaa(X1, X2, X3, X4, X5, X6, X9, mergesortcE_out_gaa(X7, X10, X6)) → U36_gaa(X1, X2, X3, X4, X5, X6, mergecC_in_ggaaa(X9, X10, X4, X5, X6))
U36_gaa(X1, X2, X3, X4, X5, X6, mergecC_out_ggaaa(X9, X10, X4, X5, X6)) → mergesortcB_out_gaa(.(X1, .(X2, X3)), X4, .(X5, X6))
Infinitary Constructor Rewriting Termination of PiDP implies Termination of TRIPLES
MERGESORTB_IN_GAA(.(X1, .(X2, X3)), X4, .(X5, X6)) → U24_GAA(X1, X2, X3, X4, X5, X6, splitD_in_ggaaa(X2, X3, X7, X8, X6))
MERGESORTB_IN_GAA(.(X1, .(X2, X3)), X4, .(X5, X6)) → SPLITD_IN_GGAAA(X2, X3, X7, X8, X6)
SPLITD_IN_GGAAA(X1, X2, .(X1, X3), X4, .(X5, X6)) → U2_GGAAA(X1, X2, X3, X4, X5, X6, splitA_in_gaaa(X2, X4, X3, X6))
SPLITD_IN_GGAAA(X1, X2, .(X1, X3), X4, .(X5, X6)) → SPLITA_IN_GAAA(X2, X4, X3, X6)
SPLITA_IN_GAAA(.(X1, X2), .(X1, X3), X4, .(X5, X6)) → U1_GAAA(X1, X2, X3, X4, X5, X6, splitA_in_gaaa(X2, X4, X3, X6))
SPLITA_IN_GAAA(.(X1, X2), .(X1, X3), X4, .(X5, X6)) → SPLITA_IN_GAAA(X2, X4, X3, X6)
MERGESORTB_IN_GAA(.(X1, .(X2, X3)), X4, .(X5, X6)) → U25_GAA(X1, X2, X3, X4, X5, X6, splitcD_in_ggaaa(X2, X3, X7, X8, X6))
U25_GAA(X1, X2, X3, X4, X5, X6, splitcD_out_ggaaa(X2, X3, X7, X8, X6)) → U26_GAA(X1, X2, X3, X4, X5, X6, mergesortB_in_gaa(.(X1, X8), X9, X6))
U25_GAA(X1, X2, X3, X4, X5, X6, splitcD_out_ggaaa(X2, X3, X7, X8, X6)) → MERGESORTB_IN_GAA(.(X1, X8), X9, X6)
U25_GAA(X1, X2, X3, X4, X5, X6, splitcD_out_ggaaa(X2, X3, X7, X8, X6)) → U27_GAA(X1, X2, X3, X4, X5, X6, X7, mergesortcB_in_gaa(.(X1, X8), X9, X6))
U27_GAA(X1, X2, X3, X4, X5, X6, X7, mergesortcB_out_gaa(.(X1, X8), X9, X6)) → U28_GAA(X1, X2, X3, X4, X5, X6, mergesortE_in_gaa(X7, X10, X6))
U27_GAA(X1, X2, X3, X4, X5, X6, X7, mergesortcB_out_gaa(.(X1, X8), X9, X6)) → MERGESORTE_IN_GAA(X7, X10, X6)
MERGESORTE_IN_GAA(.(X1, .(X2, X3)), X4, .(X5, X6)) → U3_GAA(X1, X2, X3, X4, X5, X6, splitD_in_ggaaa(X1, .(X2, X3), X7, X8, .(X5, X6)))
MERGESORTE_IN_GAA(.(X1, .(X2, X3)), X4, .(X5, X6)) → SPLITD_IN_GGAAA(X1, .(X2, X3), X7, X8, .(X5, X6))
MERGESORTE_IN_GAA(.(X1, .(X2, X3)), X4, .(X5, X6)) → U4_GAA(X1, X2, X3, X4, X5, X6, splitcD_in_ggaaa(X1, .(X2, X3), X7, X8, .(X5, X6)))
U4_GAA(X1, X2, X3, X4, X5, X6, splitcD_out_ggaaa(X1, .(X2, X3), X7, X8, .(X5, X6))) → U5_GAA(X1, X2, X3, X4, X5, X6, mergesortE_in_gaa(X7, X9, X6))
U4_GAA(X1, X2, X3, X4, X5, X6, splitcD_out_ggaaa(X1, .(X2, X3), X7, X8, .(X5, X6))) → MERGESORTE_IN_GAA(X7, X9, X6)
U4_GAA(X1, X2, X3, X4, X5, X6, splitcD_out_ggaaa(X1, .(X2, X3), X7, X8, .(X5, X6))) → U6_GAA(X1, X2, X3, X4, X5, X6, X8, mergesortcE_in_gaa(X7, X9, X6))
U6_GAA(X1, X2, X3, X4, X5, X6, X8, mergesortcE_out_gaa(X7, X9, X6)) → U7_GAA(X1, X2, X3, X4, X5, X6, mergesortE_in_gaa(X8, X10, X6))
U6_GAA(X1, X2, X3, X4, X5, X6, X8, mergesortcE_out_gaa(X7, X9, X6)) → MERGESORTE_IN_GAA(X8, X10, X6)
U6_GAA(X1, X2, X3, X4, X5, X6, X8, mergesortcE_out_gaa(X7, X9, X6)) → U8_GAA(X1, X2, X3, X4, X5, X6, X9, mergesortcE_in_gaa(X8, X10, X6))
U8_GAA(X1, X2, X3, X4, X5, X6, X9, mergesortcE_out_gaa(X8, X10, X6)) → U9_GAA(X1, X2, X3, X4, X5, X6, mergeC_in_ggaaa(X9, X10, X4, X5, X6))
U8_GAA(X1, X2, X3, X4, X5, X6, X9, mergesortcE_out_gaa(X8, X10, X6)) → MERGEC_IN_GGAAA(X9, X10, X4, X5, X6)
MERGEC_IN_GGAAA(.(X1, X2), .(X3, X4), .(X1, X5), X6, X7) → U10_GGAAA(X1, X2, X3, X4, X5, X6, X7, pF_in_ggggaa(X1, X3, X2, X4, X5, X7))
MERGEC_IN_GGAAA(.(X1, X2), .(X3, X4), .(X1, X5), X6, X7) → PF_IN_GGGGAA(X1, X3, X2, X4, X5, X7)
PF_IN_GGGGAA(X1, X2, X3, X4, X5, X6) → U13_GGGGAA(X1, X2, X3, X4, X5, X6, leH_in_gg(X1, X2))
PF_IN_GGGGAA(X1, X2, X3, X4, X5, X6) → LEH_IN_GG(X1, X2)
LEH_IN_GG(s(X1), s(X2)) → U12_GG(X1, X2, leH_in_gg(X1, X2))
LEH_IN_GG(s(X1), s(X2)) → LEH_IN_GG(X1, X2)
PF_IN_GGGGAA(X1, X2, .(X3, X4), X5, .(X3, X6), .(X7, X8)) → U14_GGGGAA(X1, X2, X3, X4, X5, X6, X7, X8, lecH_in_gg(X1, X2))
U14_GGGGAA(X1, X2, X3, X4, X5, X6, X7, X8, lecH_out_gg(X1, X2)) → U15_GGGGAA(X1, X2, X3, X4, X5, X6, X7, X8, pF_in_ggggaa(X3, X2, X4, X5, X6, X8))
U14_GGGGAA(X1, X2, X3, X4, X5, X6, X7, X8, lecH_out_gg(X1, X2)) → PF_IN_GGGGAA(X3, X2, X4, X5, X6, X8)
PF_IN_GGGGAA(X1, X2, .(X3, X4), X5, .(X2, X6), .(X7, X8)) → U16_GGGGAA(X1, X2, X3, X4, X5, X6, X7, X8, lecH_in_gg(X1, X2))
U16_GGGGAA(X1, X2, X3, X4, X5, X6, X7, X8, lecH_out_gg(X1, X2)) → U17_GGGGAA(X1, X2, X3, X4, X5, X6, X7, X8, pG_in_ggggaa(X3, X2, X4, X5, X6, X8))
U16_GGGGAA(X1, X2, X3, X4, X5, X6, X7, X8, lecH_out_gg(X1, X2)) → PG_IN_GGGGAA(X3, X2, X4, X5, X6, X8)
PG_IN_GGGGAA(X1, X2, X3, X4, X5, X6) → U19_GGGGAA(X1, X2, X3, X4, X5, X6, gtI_in_gg(X1, X2))
PG_IN_GGGGAA(X1, X2, X3, X4, X5, X6) → GTI_IN_GG(X1, X2)
GTI_IN_GG(s(X1), s(X2)) → U18_GG(X1, X2, gtI_in_gg(X1, X2))
GTI_IN_GG(s(X1), s(X2)) → GTI_IN_GG(X1, X2)
PG_IN_GGGGAA(X1, X2, X3, .(X4, X5), .(X1, X6), .(X7, X8)) → U20_GGGGAA(X1, X2, X3, X4, X5, X6, X7, X8, gtcI_in_gg(X1, X2))
U20_GGGGAA(X1, X2, X3, X4, X5, X6, X7, X8, gtcI_out_gg(X1, X2)) → U21_GGGGAA(X1, X2, X3, X4, X5, X6, X7, X8, pF_in_ggggaa(X1, X4, X3, X5, X6, X8))
U20_GGGGAA(X1, X2, X3, X4, X5, X6, X7, X8, gtcI_out_gg(X1, X2)) → PF_IN_GGGGAA(X1, X4, X3, X5, X6, X8)
PG_IN_GGGGAA(X1, X2, X3, .(X4, X5), .(X4, X6), .(X7, X8)) → U22_GGGGAA(X1, X2, X3, X4, X5, X6, X7, X8, gtcI_in_gg(X1, X2))
U22_GGGGAA(X1, X2, X3, X4, X5, X6, X7, X8, gtcI_out_gg(X1, X2)) → U23_GGGGAA(X1, X2, X3, X4, X5, X6, X7, X8, pG_in_ggggaa(X1, X4, X3, X5, X6, X8))
U22_GGGGAA(X1, X2, X3, X4, X5, X6, X7, X8, gtcI_out_gg(X1, X2)) → PG_IN_GGGGAA(X1, X4, X3, X5, X6, X8)
MERGEC_IN_GGAAA(.(X1, X2), .(X3, X4), .(X3, X5), X6, X7) → U11_GGAAA(X1, X2, X3, X4, X5, X6, X7, pG_in_ggggaa(X1, X3, X2, X4, X5, X7))
MERGEC_IN_GGAAA(.(X1, X2), .(X3, X4), .(X3, X5), X6, X7) → PG_IN_GGGGAA(X1, X3, X2, X4, X5, X7)
U27_GAA(X1, X2, X3, X4, X5, X6, X7, mergesortcB_out_gaa(.(X1, X8), X9, X6)) → U29_GAA(X1, X2, X3, X4, X5, X6, X9, mergesortcE_in_gaa(X7, X10, X6))
U29_GAA(X1, X2, X3, X4, X5, X6, X9, mergesortcE_out_gaa(X7, X10, X6)) → U30_GAA(X1, X2, X3, X4, X5, X6, mergeC_in_ggaaa(X9, X10, X4, X5, X6))
U29_GAA(X1, X2, X3, X4, X5, X6, X9, mergesortcE_out_gaa(X7, X10, X6)) → MERGEC_IN_GGAAA(X9, X10, X4, X5, X6)
splitcD_in_ggaaa(X1, X2, .(X1, X3), X4, .(X5, X6)) → U37_ggaaa(X1, X2, X3, X4, X5, X6, splitcA_in_gaaa(X2, X4, X3, X6))
splitcA_in_gaaa([], [], [], X1) → splitcA_out_gaaa([], [], [], X1)
splitcA_in_gaaa(.(X1, X2), .(X1, X3), X4, .(X5, X6)) → U32_gaaa(X1, X2, X3, X4, X5, X6, splitcA_in_gaaa(X2, X4, X3, X6))
U32_gaaa(X1, X2, X3, X4, X5, X6, splitcA_out_gaaa(X2, X4, X3, X6)) → splitcA_out_gaaa(.(X1, X2), .(X1, X3), X4, .(X5, X6))
U37_ggaaa(X1, X2, X3, X4, X5, X6, splitcA_out_gaaa(X2, X4, X3, X6)) → splitcD_out_ggaaa(X1, X2, .(X1, X3), X4, .(X5, X6))
mergesortcB_in_gaa([], [], X1) → mergesortcB_out_gaa([], [], X1)
mergesortcB_in_gaa(.(X1, []), .(X1, []), X2) → mergesortcB_out_gaa(.(X1, []), .(X1, []), X2)
mergesortcB_in_gaa(.(X1, .(X2, X3)), X4, .(X5, X6)) → U33_gaa(X1, X2, X3, X4, X5, X6, splitcD_in_ggaaa(X2, X3, X7, X8, X6))
U33_gaa(X1, X2, X3, X4, X5, X6, splitcD_out_ggaaa(X2, X3, X7, X8, X6)) → U34_gaa(X1, X2, X3, X4, X5, X6, X7, mergesortcB_in_gaa(.(X1, X8), X9, X6))
U34_gaa(X1, X2, X3, X4, X5, X6, X7, mergesortcB_out_gaa(.(X1, X8), X9, X6)) → U35_gaa(X1, X2, X3, X4, X5, X6, X9, mergesortcE_in_gaa(X7, X10, X6))
mergesortcE_in_gaa([], [], X1) → mergesortcE_out_gaa([], [], X1)
mergesortcE_in_gaa(.(X1, []), .(X1, []), X2) → mergesortcE_out_gaa(.(X1, []), .(X1, []), X2)
mergesortcE_in_gaa(.(X1, .(X2, X3)), X4, .(X5, X6)) → U38_gaa(X1, X2, X3, X4, X5, X6, splitcD_in_ggaaa(X1, .(X2, X3), X7, X8, .(X5, X6)))
U38_gaa(X1, X2, X3, X4, X5, X6, splitcD_out_ggaaa(X1, .(X2, X3), X7, X8, .(X5, X6))) → U39_gaa(X1, X2, X3, X4, X5, X6, X8, mergesortcE_in_gaa(X7, X9, X6))
U39_gaa(X1, X2, X3, X4, X5, X6, X8, mergesortcE_out_gaa(X7, X9, X6)) → U40_gaa(X1, X2, X3, X4, X5, X6, X9, mergesortcE_in_gaa(X8, X10, X6))
U40_gaa(X1, X2, X3, X4, X5, X6, X9, mergesortcE_out_gaa(X8, X10, X6)) → U41_gaa(X1, X2, X3, X4, X5, X6, mergecC_in_ggaaa(X9, X10, X4, X5, X6))
mergecC_in_ggaaa([], X1, X1, X2, X3) → mergecC_out_ggaaa([], X1, X1, X2, X3)
mergecC_in_ggaaa(X1, [], X1, X2, X3) → mergecC_out_ggaaa(X1, [], X1, X2, X3)
mergecC_in_ggaaa(.(X1, X2), .(X3, X4), .(X1, X5), X6, X7) → U42_ggaaa(X1, X2, X3, X4, X5, X6, X7, qcF_in_ggggaa(X1, X3, X2, X4, X5, X7))
qcF_in_ggggaa(X1, X2, [], X3, .(X2, X3), X4) → U45_ggggaa(X1, X2, X3, X4, lecH_in_gg(X1, X2))
lecH_in_gg(s(X1), s(X2)) → U44_gg(X1, X2, lecH_in_gg(X1, X2))
lecH_in_gg(0, s(0)) → lecH_out_gg(0, s(0))
lecH_in_gg(0, 0) → lecH_out_gg(0, 0)
U44_gg(X1, X2, lecH_out_gg(X1, X2)) → lecH_out_gg(s(X1), s(X2))
U45_ggggaa(X1, X2, X3, X4, lecH_out_gg(X1, X2)) → qcF_out_ggggaa(X1, X2, [], X3, .(X2, X3), X4)
qcF_in_ggggaa(X1, X2, .(X3, X4), X5, .(X3, X6), .(X7, X8)) → U46_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, lecH_in_gg(X1, X2))
U46_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, lecH_out_gg(X1, X2)) → U47_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, qcF_in_ggggaa(X3, X2, X4, X5, X6, X8))
qcF_in_ggggaa(X1, X2, .(X3, X4), X5, .(X2, X6), .(X7, X8)) → U48_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, lecH_in_gg(X1, X2))
U48_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, lecH_out_gg(X1, X2)) → U49_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, qcG_in_ggggaa(X3, X2, X4, X5, X6, X8))
qcG_in_ggggaa(X1, X2, X3, [], .(X1, X3), X4) → U51_ggggaa(X1, X2, X3, X4, gtcI_in_gg(X1, X2))
gtcI_in_gg(s(X1), s(X2)) → U50_gg(X1, X2, gtcI_in_gg(X1, X2))
gtcI_in_gg(s(0), 0) → gtcI_out_gg(s(0), 0)
U50_gg(X1, X2, gtcI_out_gg(X1, X2)) → gtcI_out_gg(s(X1), s(X2))
U51_ggggaa(X1, X2, X3, X4, gtcI_out_gg(X1, X2)) → qcG_out_ggggaa(X1, X2, X3, [], .(X1, X3), X4)
qcG_in_ggggaa(X1, X2, X3, .(X4, X5), .(X1, X6), .(X7, X8)) → U52_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, gtcI_in_gg(X1, X2))
U52_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, gtcI_out_gg(X1, X2)) → U53_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, qcF_in_ggggaa(X1, X4, X3, X5, X6, X8))
U53_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, qcF_out_ggggaa(X1, X4, X3, X5, X6, X8)) → qcG_out_ggggaa(X1, X2, X3, .(X4, X5), .(X1, X6), .(X7, X8))
qcG_in_ggggaa(X1, X2, X3, .(X4, X5), .(X4, X6), .(X7, X8)) → U54_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, gtcI_in_gg(X1, X2))
U54_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, gtcI_out_gg(X1, X2)) → U55_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, qcG_in_ggggaa(X1, X4, X3, X5, X6, X8))
U55_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, qcG_out_ggggaa(X1, X4, X3, X5, X6, X8)) → qcG_out_ggggaa(X1, X2, X3, .(X4, X5), .(X4, X6), .(X7, X8))
U49_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, qcG_out_ggggaa(X3, X2, X4, X5, X6, X8)) → qcF_out_ggggaa(X1, X2, .(X3, X4), X5, .(X2, X6), .(X7, X8))
U47_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, qcF_out_ggggaa(X3, X2, X4, X5, X6, X8)) → qcF_out_ggggaa(X1, X2, .(X3, X4), X5, .(X3, X6), .(X7, X8))
U42_ggaaa(X1, X2, X3, X4, X5, X6, X7, qcF_out_ggggaa(X1, X3, X2, X4, X5, X7)) → mergecC_out_ggaaa(.(X1, X2), .(X3, X4), .(X1, X5), X6, X7)
mergecC_in_ggaaa(.(X1, X2), .(X3, X4), .(X3, X5), X6, X7) → U43_ggaaa(X1, X2, X3, X4, X5, X6, X7, qcG_in_ggggaa(X1, X3, X2, X4, X5, X7))
U43_ggaaa(X1, X2, X3, X4, X5, X6, X7, qcG_out_ggggaa(X1, X3, X2, X4, X5, X7)) → mergecC_out_ggaaa(.(X1, X2), .(X3, X4), .(X3, X5), X6, X7)
U41_gaa(X1, X2, X3, X4, X5, X6, mergecC_out_ggaaa(X9, X10, X4, X5, X6)) → mergesortcE_out_gaa(.(X1, .(X2, X3)), X4, .(X5, X6))
U35_gaa(X1, X2, X3, X4, X5, X6, X9, mergesortcE_out_gaa(X7, X10, X6)) → U36_gaa(X1, X2, X3, X4, X5, X6, mergecC_in_ggaaa(X9, X10, X4, X5, X6))
U36_gaa(X1, X2, X3, X4, X5, X6, mergecC_out_ggaaa(X9, X10, X4, X5, X6)) → mergesortcB_out_gaa(.(X1, .(X2, X3)), X4, .(X5, X6))
GTI_IN_GG(s(X1), s(X2)) → GTI_IN_GG(X1, X2)
splitcD_in_ggaaa(X1, X2, .(X1, X3), X4, .(X5, X6)) → U37_ggaaa(X1, X2, X3, X4, X5, X6, splitcA_in_gaaa(X2, X4, X3, X6))
splitcA_in_gaaa([], [], [], X1) → splitcA_out_gaaa([], [], [], X1)
splitcA_in_gaaa(.(X1, X2), .(X1, X3), X4, .(X5, X6)) → U32_gaaa(X1, X2, X3, X4, X5, X6, splitcA_in_gaaa(X2, X4, X3, X6))
U32_gaaa(X1, X2, X3, X4, X5, X6, splitcA_out_gaaa(X2, X4, X3, X6)) → splitcA_out_gaaa(.(X1, X2), .(X1, X3), X4, .(X5, X6))
U37_ggaaa(X1, X2, X3, X4, X5, X6, splitcA_out_gaaa(X2, X4, X3, X6)) → splitcD_out_ggaaa(X1, X2, .(X1, X3), X4, .(X5, X6))
mergesortcB_in_gaa([], [], X1) → mergesortcB_out_gaa([], [], X1)
mergesortcB_in_gaa(.(X1, []), .(X1, []), X2) → mergesortcB_out_gaa(.(X1, []), .(X1, []), X2)
mergesortcB_in_gaa(.(X1, .(X2, X3)), X4, .(X5, X6)) → U33_gaa(X1, X2, X3, X4, X5, X6, splitcD_in_ggaaa(X2, X3, X7, X8, X6))
U33_gaa(X1, X2, X3, X4, X5, X6, splitcD_out_ggaaa(X2, X3, X7, X8, X6)) → U34_gaa(X1, X2, X3, X4, X5, X6, X7, mergesortcB_in_gaa(.(X1, X8), X9, X6))
U34_gaa(X1, X2, X3, X4, X5, X6, X7, mergesortcB_out_gaa(.(X1, X8), X9, X6)) → U35_gaa(X1, X2, X3, X4, X5, X6, X9, mergesortcE_in_gaa(X7, X10, X6))
mergesortcE_in_gaa([], [], X1) → mergesortcE_out_gaa([], [], X1)
mergesortcE_in_gaa(.(X1, []), .(X1, []), X2) → mergesortcE_out_gaa(.(X1, []), .(X1, []), X2)
mergesortcE_in_gaa(.(X1, .(X2, X3)), X4, .(X5, X6)) → U38_gaa(X1, X2, X3, X4, X5, X6, splitcD_in_ggaaa(X1, .(X2, X3), X7, X8, .(X5, X6)))
U38_gaa(X1, X2, X3, X4, X5, X6, splitcD_out_ggaaa(X1, .(X2, X3), X7, X8, .(X5, X6))) → U39_gaa(X1, X2, X3, X4, X5, X6, X8, mergesortcE_in_gaa(X7, X9, X6))
U39_gaa(X1, X2, X3, X4, X5, X6, X8, mergesortcE_out_gaa(X7, X9, X6)) → U40_gaa(X1, X2, X3, X4, X5, X6, X9, mergesortcE_in_gaa(X8, X10, X6))
U40_gaa(X1, X2, X3, X4, X5, X6, X9, mergesortcE_out_gaa(X8, X10, X6)) → U41_gaa(X1, X2, X3, X4, X5, X6, mergecC_in_ggaaa(X9, X10, X4, X5, X6))
mergecC_in_ggaaa([], X1, X1, X2, X3) → mergecC_out_ggaaa([], X1, X1, X2, X3)
mergecC_in_ggaaa(X1, [], X1, X2, X3) → mergecC_out_ggaaa(X1, [], X1, X2, X3)
mergecC_in_ggaaa(.(X1, X2), .(X3, X4), .(X1, X5), X6, X7) → U42_ggaaa(X1, X2, X3, X4, X5, X6, X7, qcF_in_ggggaa(X1, X3, X2, X4, X5, X7))
qcF_in_ggggaa(X1, X2, [], X3, .(X2, X3), X4) → U45_ggggaa(X1, X2, X3, X4, lecH_in_gg(X1, X2))
lecH_in_gg(s(X1), s(X2)) → U44_gg(X1, X2, lecH_in_gg(X1, X2))
lecH_in_gg(0, s(0)) → lecH_out_gg(0, s(0))
lecH_in_gg(0, 0) → lecH_out_gg(0, 0)
U44_gg(X1, X2, lecH_out_gg(X1, X2)) → lecH_out_gg(s(X1), s(X2))
U45_ggggaa(X1, X2, X3, X4, lecH_out_gg(X1, X2)) → qcF_out_ggggaa(X1, X2, [], X3, .(X2, X3), X4)
qcF_in_ggggaa(X1, X2, .(X3, X4), X5, .(X3, X6), .(X7, X8)) → U46_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, lecH_in_gg(X1, X2))
U46_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, lecH_out_gg(X1, X2)) → U47_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, qcF_in_ggggaa(X3, X2, X4, X5, X6, X8))
qcF_in_ggggaa(X1, X2, .(X3, X4), X5, .(X2, X6), .(X7, X8)) → U48_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, lecH_in_gg(X1, X2))
U48_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, lecH_out_gg(X1, X2)) → U49_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, qcG_in_ggggaa(X3, X2, X4, X5, X6, X8))
qcG_in_ggggaa(X1, X2, X3, [], .(X1, X3), X4) → U51_ggggaa(X1, X2, X3, X4, gtcI_in_gg(X1, X2))
gtcI_in_gg(s(X1), s(X2)) → U50_gg(X1, X2, gtcI_in_gg(X1, X2))
gtcI_in_gg(s(0), 0) → gtcI_out_gg(s(0), 0)
U50_gg(X1, X2, gtcI_out_gg(X1, X2)) → gtcI_out_gg(s(X1), s(X2))
U51_ggggaa(X1, X2, X3, X4, gtcI_out_gg(X1, X2)) → qcG_out_ggggaa(X1, X2, X3, [], .(X1, X3), X4)
qcG_in_ggggaa(X1, X2, X3, .(X4, X5), .(X1, X6), .(X7, X8)) → U52_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, gtcI_in_gg(X1, X2))
U52_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, gtcI_out_gg(X1, X2)) → U53_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, qcF_in_ggggaa(X1, X4, X3, X5, X6, X8))
U53_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, qcF_out_ggggaa(X1, X4, X3, X5, X6, X8)) → qcG_out_ggggaa(X1, X2, X3, .(X4, X5), .(X1, X6), .(X7, X8))
qcG_in_ggggaa(X1, X2, X3, .(X4, X5), .(X4, X6), .(X7, X8)) → U54_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, gtcI_in_gg(X1, X2))
U54_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, gtcI_out_gg(X1, X2)) → U55_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, qcG_in_ggggaa(X1, X4, X3, X5, X6, X8))
U55_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, qcG_out_ggggaa(X1, X4, X3, X5, X6, X8)) → qcG_out_ggggaa(X1, X2, X3, .(X4, X5), .(X4, X6), .(X7, X8))
U49_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, qcG_out_ggggaa(X3, X2, X4, X5, X6, X8)) → qcF_out_ggggaa(X1, X2, .(X3, X4), X5, .(X2, X6), .(X7, X8))
U47_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, qcF_out_ggggaa(X3, X2, X4, X5, X6, X8)) → qcF_out_ggggaa(X1, X2, .(X3, X4), X5, .(X3, X6), .(X7, X8))
U42_ggaaa(X1, X2, X3, X4, X5, X6, X7, qcF_out_ggggaa(X1, X3, X2, X4, X5, X7)) → mergecC_out_ggaaa(.(X1, X2), .(X3, X4), .(X1, X5), X6, X7)
mergecC_in_ggaaa(.(X1, X2), .(X3, X4), .(X3, X5), X6, X7) → U43_ggaaa(X1, X2, X3, X4, X5, X6, X7, qcG_in_ggggaa(X1, X3, X2, X4, X5, X7))
U43_ggaaa(X1, X2, X3, X4, X5, X6, X7, qcG_out_ggggaa(X1, X3, X2, X4, X5, X7)) → mergecC_out_ggaaa(.(X1, X2), .(X3, X4), .(X3, X5), X6, X7)
U41_gaa(X1, X2, X3, X4, X5, X6, mergecC_out_ggaaa(X9, X10, X4, X5, X6)) → mergesortcE_out_gaa(.(X1, .(X2, X3)), X4, .(X5, X6))
U35_gaa(X1, X2, X3, X4, X5, X6, X9, mergesortcE_out_gaa(X7, X10, X6)) → U36_gaa(X1, X2, X3, X4, X5, X6, mergecC_in_ggaaa(X9, X10, X4, X5, X6))
U36_gaa(X1, X2, X3, X4, X5, X6, mergecC_out_ggaaa(X9, X10, X4, X5, X6)) → mergesortcB_out_gaa(.(X1, .(X2, X3)), X4, .(X5, X6))
GTI_IN_GG(s(X1), s(X2)) → GTI_IN_GG(X1, X2)
GTI_IN_GG(s(X1), s(X2)) → GTI_IN_GG(X1, X2)
From the DPs we obtained the following set of size-change graphs:
LEH_IN_GG(s(X1), s(X2)) → LEH_IN_GG(X1, X2)
splitcD_in_ggaaa(X1, X2, .(X1, X3), X4, .(X5, X6)) → U37_ggaaa(X1, X2, X3, X4, X5, X6, splitcA_in_gaaa(X2, X4, X3, X6))
splitcA_in_gaaa([], [], [], X1) → splitcA_out_gaaa([], [], [], X1)
splitcA_in_gaaa(.(X1, X2), .(X1, X3), X4, .(X5, X6)) → U32_gaaa(X1, X2, X3, X4, X5, X6, splitcA_in_gaaa(X2, X4, X3, X6))
U32_gaaa(X1, X2, X3, X4, X5, X6, splitcA_out_gaaa(X2, X4, X3, X6)) → splitcA_out_gaaa(.(X1, X2), .(X1, X3), X4, .(X5, X6))
U37_ggaaa(X1, X2, X3, X4, X5, X6, splitcA_out_gaaa(X2, X4, X3, X6)) → splitcD_out_ggaaa(X1, X2, .(X1, X3), X4, .(X5, X6))
mergesortcB_in_gaa([], [], X1) → mergesortcB_out_gaa([], [], X1)
mergesortcB_in_gaa(.(X1, []), .(X1, []), X2) → mergesortcB_out_gaa(.(X1, []), .(X1, []), X2)
mergesortcB_in_gaa(.(X1, .(X2, X3)), X4, .(X5, X6)) → U33_gaa(X1, X2, X3, X4, X5, X6, splitcD_in_ggaaa(X2, X3, X7, X8, X6))
U33_gaa(X1, X2, X3, X4, X5, X6, splitcD_out_ggaaa(X2, X3, X7, X8, X6)) → U34_gaa(X1, X2, X3, X4, X5, X6, X7, mergesortcB_in_gaa(.(X1, X8), X9, X6))
U34_gaa(X1, X2, X3, X4, X5, X6, X7, mergesortcB_out_gaa(.(X1, X8), X9, X6)) → U35_gaa(X1, X2, X3, X4, X5, X6, X9, mergesortcE_in_gaa(X7, X10, X6))
mergesortcE_in_gaa([], [], X1) → mergesortcE_out_gaa([], [], X1)
mergesortcE_in_gaa(.(X1, []), .(X1, []), X2) → mergesortcE_out_gaa(.(X1, []), .(X1, []), X2)
mergesortcE_in_gaa(.(X1, .(X2, X3)), X4, .(X5, X6)) → U38_gaa(X1, X2, X3, X4, X5, X6, splitcD_in_ggaaa(X1, .(X2, X3), X7, X8, .(X5, X6)))
U38_gaa(X1, X2, X3, X4, X5, X6, splitcD_out_ggaaa(X1, .(X2, X3), X7, X8, .(X5, X6))) → U39_gaa(X1, X2, X3, X4, X5, X6, X8, mergesortcE_in_gaa(X7, X9, X6))
U39_gaa(X1, X2, X3, X4, X5, X6, X8, mergesortcE_out_gaa(X7, X9, X6)) → U40_gaa(X1, X2, X3, X4, X5, X6, X9, mergesortcE_in_gaa(X8, X10, X6))
U40_gaa(X1, X2, X3, X4, X5, X6, X9, mergesortcE_out_gaa(X8, X10, X6)) → U41_gaa(X1, X2, X3, X4, X5, X6, mergecC_in_ggaaa(X9, X10, X4, X5, X6))
mergecC_in_ggaaa([], X1, X1, X2, X3) → mergecC_out_ggaaa([], X1, X1, X2, X3)
mergecC_in_ggaaa(X1, [], X1, X2, X3) → mergecC_out_ggaaa(X1, [], X1, X2, X3)
mergecC_in_ggaaa(.(X1, X2), .(X3, X4), .(X1, X5), X6, X7) → U42_ggaaa(X1, X2, X3, X4, X5, X6, X7, qcF_in_ggggaa(X1, X3, X2, X4, X5, X7))
qcF_in_ggggaa(X1, X2, [], X3, .(X2, X3), X4) → U45_ggggaa(X1, X2, X3, X4, lecH_in_gg(X1, X2))
lecH_in_gg(s(X1), s(X2)) → U44_gg(X1, X2, lecH_in_gg(X1, X2))
lecH_in_gg(0, s(0)) → lecH_out_gg(0, s(0))
lecH_in_gg(0, 0) → lecH_out_gg(0, 0)
U44_gg(X1, X2, lecH_out_gg(X1, X2)) → lecH_out_gg(s(X1), s(X2))
U45_ggggaa(X1, X2, X3, X4, lecH_out_gg(X1, X2)) → qcF_out_ggggaa(X1, X2, [], X3, .(X2, X3), X4)
qcF_in_ggggaa(X1, X2, .(X3, X4), X5, .(X3, X6), .(X7, X8)) → U46_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, lecH_in_gg(X1, X2))
U46_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, lecH_out_gg(X1, X2)) → U47_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, qcF_in_ggggaa(X3, X2, X4, X5, X6, X8))
qcF_in_ggggaa(X1, X2, .(X3, X4), X5, .(X2, X6), .(X7, X8)) → U48_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, lecH_in_gg(X1, X2))
U48_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, lecH_out_gg(X1, X2)) → U49_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, qcG_in_ggggaa(X3, X2, X4, X5, X6, X8))
qcG_in_ggggaa(X1, X2, X3, [], .(X1, X3), X4) → U51_ggggaa(X1, X2, X3, X4, gtcI_in_gg(X1, X2))
gtcI_in_gg(s(X1), s(X2)) → U50_gg(X1, X2, gtcI_in_gg(X1, X2))
gtcI_in_gg(s(0), 0) → gtcI_out_gg(s(0), 0)
U50_gg(X1, X2, gtcI_out_gg(X1, X2)) → gtcI_out_gg(s(X1), s(X2))
U51_ggggaa(X1, X2, X3, X4, gtcI_out_gg(X1, X2)) → qcG_out_ggggaa(X1, X2, X3, [], .(X1, X3), X4)
qcG_in_ggggaa(X1, X2, X3, .(X4, X5), .(X1, X6), .(X7, X8)) → U52_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, gtcI_in_gg(X1, X2))
U52_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, gtcI_out_gg(X1, X2)) → U53_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, qcF_in_ggggaa(X1, X4, X3, X5, X6, X8))
U53_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, qcF_out_ggggaa(X1, X4, X3, X5, X6, X8)) → qcG_out_ggggaa(X1, X2, X3, .(X4, X5), .(X1, X6), .(X7, X8))
qcG_in_ggggaa(X1, X2, X3, .(X4, X5), .(X4, X6), .(X7, X8)) → U54_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, gtcI_in_gg(X1, X2))
U54_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, gtcI_out_gg(X1, X2)) → U55_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, qcG_in_ggggaa(X1, X4, X3, X5, X6, X8))
U55_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, qcG_out_ggggaa(X1, X4, X3, X5, X6, X8)) → qcG_out_ggggaa(X1, X2, X3, .(X4, X5), .(X4, X6), .(X7, X8))
U49_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, qcG_out_ggggaa(X3, X2, X4, X5, X6, X8)) → qcF_out_ggggaa(X1, X2, .(X3, X4), X5, .(X2, X6), .(X7, X8))
U47_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, qcF_out_ggggaa(X3, X2, X4, X5, X6, X8)) → qcF_out_ggggaa(X1, X2, .(X3, X4), X5, .(X3, X6), .(X7, X8))
U42_ggaaa(X1, X2, X3, X4, X5, X6, X7, qcF_out_ggggaa(X1, X3, X2, X4, X5, X7)) → mergecC_out_ggaaa(.(X1, X2), .(X3, X4), .(X1, X5), X6, X7)
mergecC_in_ggaaa(.(X1, X2), .(X3, X4), .(X3, X5), X6, X7) → U43_ggaaa(X1, X2, X3, X4, X5, X6, X7, qcG_in_ggggaa(X1, X3, X2, X4, X5, X7))
U43_ggaaa(X1, X2, X3, X4, X5, X6, X7, qcG_out_ggggaa(X1, X3, X2, X4, X5, X7)) → mergecC_out_ggaaa(.(X1, X2), .(X3, X4), .(X3, X5), X6, X7)
U41_gaa(X1, X2, X3, X4, X5, X6, mergecC_out_ggaaa(X9, X10, X4, X5, X6)) → mergesortcE_out_gaa(.(X1, .(X2, X3)), X4, .(X5, X6))
U35_gaa(X1, X2, X3, X4, X5, X6, X9, mergesortcE_out_gaa(X7, X10, X6)) → U36_gaa(X1, X2, X3, X4, X5, X6, mergecC_in_ggaaa(X9, X10, X4, X5, X6))
U36_gaa(X1, X2, X3, X4, X5, X6, mergecC_out_ggaaa(X9, X10, X4, X5, X6)) → mergesortcB_out_gaa(.(X1, .(X2, X3)), X4, .(X5, X6))
LEH_IN_GG(s(X1), s(X2)) → LEH_IN_GG(X1, X2)
LEH_IN_GG(s(X1), s(X2)) → LEH_IN_GG(X1, X2)
From the DPs we obtained the following set of size-change graphs:
PF_IN_GGGGAA(X1, X2, .(X3, X4), X5, .(X3, X6), .(X7, X8)) → U14_GGGGAA(X1, X2, X3, X4, X5, X6, X7, X8, lecH_in_gg(X1, X2))
U14_GGGGAA(X1, X2, X3, X4, X5, X6, X7, X8, lecH_out_gg(X1, X2)) → PF_IN_GGGGAA(X3, X2, X4, X5, X6, X8)
PF_IN_GGGGAA(X1, X2, .(X3, X4), X5, .(X2, X6), .(X7, X8)) → U16_GGGGAA(X1, X2, X3, X4, X5, X6, X7, X8, lecH_in_gg(X1, X2))
U16_GGGGAA(X1, X2, X3, X4, X5, X6, X7, X8, lecH_out_gg(X1, X2)) → PG_IN_GGGGAA(X3, X2, X4, X5, X6, X8)
PG_IN_GGGGAA(X1, X2, X3, .(X4, X5), .(X1, X6), .(X7, X8)) → U20_GGGGAA(X1, X2, X3, X4, X5, X6, X7, X8, gtcI_in_gg(X1, X2))
U20_GGGGAA(X1, X2, X3, X4, X5, X6, X7, X8, gtcI_out_gg(X1, X2)) → PF_IN_GGGGAA(X1, X4, X3, X5, X6, X8)
PG_IN_GGGGAA(X1, X2, X3, .(X4, X5), .(X4, X6), .(X7, X8)) → U22_GGGGAA(X1, X2, X3, X4, X5, X6, X7, X8, gtcI_in_gg(X1, X2))
U22_GGGGAA(X1, X2, X3, X4, X5, X6, X7, X8, gtcI_out_gg(X1, X2)) → PG_IN_GGGGAA(X1, X4, X3, X5, X6, X8)
splitcD_in_ggaaa(X1, X2, .(X1, X3), X4, .(X5, X6)) → U37_ggaaa(X1, X2, X3, X4, X5, X6, splitcA_in_gaaa(X2, X4, X3, X6))
splitcA_in_gaaa([], [], [], X1) → splitcA_out_gaaa([], [], [], X1)
splitcA_in_gaaa(.(X1, X2), .(X1, X3), X4, .(X5, X6)) → U32_gaaa(X1, X2, X3, X4, X5, X6, splitcA_in_gaaa(X2, X4, X3, X6))
U32_gaaa(X1, X2, X3, X4, X5, X6, splitcA_out_gaaa(X2, X4, X3, X6)) → splitcA_out_gaaa(.(X1, X2), .(X1, X3), X4, .(X5, X6))
U37_ggaaa(X1, X2, X3, X4, X5, X6, splitcA_out_gaaa(X2, X4, X3, X6)) → splitcD_out_ggaaa(X1, X2, .(X1, X3), X4, .(X5, X6))
mergesortcB_in_gaa([], [], X1) → mergesortcB_out_gaa([], [], X1)
mergesortcB_in_gaa(.(X1, []), .(X1, []), X2) → mergesortcB_out_gaa(.(X1, []), .(X1, []), X2)
mergesortcB_in_gaa(.(X1, .(X2, X3)), X4, .(X5, X6)) → U33_gaa(X1, X2, X3, X4, X5, X6, splitcD_in_ggaaa(X2, X3, X7, X8, X6))
U33_gaa(X1, X2, X3, X4, X5, X6, splitcD_out_ggaaa(X2, X3, X7, X8, X6)) → U34_gaa(X1, X2, X3, X4, X5, X6, X7, mergesortcB_in_gaa(.(X1, X8), X9, X6))
U34_gaa(X1, X2, X3, X4, X5, X6, X7, mergesortcB_out_gaa(.(X1, X8), X9, X6)) → U35_gaa(X1, X2, X3, X4, X5, X6, X9, mergesortcE_in_gaa(X7, X10, X6))
mergesortcE_in_gaa([], [], X1) → mergesortcE_out_gaa([], [], X1)
mergesortcE_in_gaa(.(X1, []), .(X1, []), X2) → mergesortcE_out_gaa(.(X1, []), .(X1, []), X2)
mergesortcE_in_gaa(.(X1, .(X2, X3)), X4, .(X5, X6)) → U38_gaa(X1, X2, X3, X4, X5, X6, splitcD_in_ggaaa(X1, .(X2, X3), X7, X8, .(X5, X6)))
U38_gaa(X1, X2, X3, X4, X5, X6, splitcD_out_ggaaa(X1, .(X2, X3), X7, X8, .(X5, X6))) → U39_gaa(X1, X2, X3, X4, X5, X6, X8, mergesortcE_in_gaa(X7, X9, X6))
U39_gaa(X1, X2, X3, X4, X5, X6, X8, mergesortcE_out_gaa(X7, X9, X6)) → U40_gaa(X1, X2, X3, X4, X5, X6, X9, mergesortcE_in_gaa(X8, X10, X6))
U40_gaa(X1, X2, X3, X4, X5, X6, X9, mergesortcE_out_gaa(X8, X10, X6)) → U41_gaa(X1, X2, X3, X4, X5, X6, mergecC_in_ggaaa(X9, X10, X4, X5, X6))
mergecC_in_ggaaa([], X1, X1, X2, X3) → mergecC_out_ggaaa([], X1, X1, X2, X3)
mergecC_in_ggaaa(X1, [], X1, X2, X3) → mergecC_out_ggaaa(X1, [], X1, X2, X3)
mergecC_in_ggaaa(.(X1, X2), .(X3, X4), .(X1, X5), X6, X7) → U42_ggaaa(X1, X2, X3, X4, X5, X6, X7, qcF_in_ggggaa(X1, X3, X2, X4, X5, X7))
qcF_in_ggggaa(X1, X2, [], X3, .(X2, X3), X4) → U45_ggggaa(X1, X2, X3, X4, lecH_in_gg(X1, X2))
lecH_in_gg(s(X1), s(X2)) → U44_gg(X1, X2, lecH_in_gg(X1, X2))
lecH_in_gg(0, s(0)) → lecH_out_gg(0, s(0))
lecH_in_gg(0, 0) → lecH_out_gg(0, 0)
U44_gg(X1, X2, lecH_out_gg(X1, X2)) → lecH_out_gg(s(X1), s(X2))
U45_ggggaa(X1, X2, X3, X4, lecH_out_gg(X1, X2)) → qcF_out_ggggaa(X1, X2, [], X3, .(X2, X3), X4)
qcF_in_ggggaa(X1, X2, .(X3, X4), X5, .(X3, X6), .(X7, X8)) → U46_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, lecH_in_gg(X1, X2))
U46_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, lecH_out_gg(X1, X2)) → U47_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, qcF_in_ggggaa(X3, X2, X4, X5, X6, X8))
qcF_in_ggggaa(X1, X2, .(X3, X4), X5, .(X2, X6), .(X7, X8)) → U48_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, lecH_in_gg(X1, X2))
U48_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, lecH_out_gg(X1, X2)) → U49_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, qcG_in_ggggaa(X3, X2, X4, X5, X6, X8))
qcG_in_ggggaa(X1, X2, X3, [], .(X1, X3), X4) → U51_ggggaa(X1, X2, X3, X4, gtcI_in_gg(X1, X2))
gtcI_in_gg(s(X1), s(X2)) → U50_gg(X1, X2, gtcI_in_gg(X1, X2))
gtcI_in_gg(s(0), 0) → gtcI_out_gg(s(0), 0)
U50_gg(X1, X2, gtcI_out_gg(X1, X2)) → gtcI_out_gg(s(X1), s(X2))
U51_ggggaa(X1, X2, X3, X4, gtcI_out_gg(X1, X2)) → qcG_out_ggggaa(X1, X2, X3, [], .(X1, X3), X4)
qcG_in_ggggaa(X1, X2, X3, .(X4, X5), .(X1, X6), .(X7, X8)) → U52_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, gtcI_in_gg(X1, X2))
U52_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, gtcI_out_gg(X1, X2)) → U53_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, qcF_in_ggggaa(X1, X4, X3, X5, X6, X8))
U53_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, qcF_out_ggggaa(X1, X4, X3, X5, X6, X8)) → qcG_out_ggggaa(X1, X2, X3, .(X4, X5), .(X1, X6), .(X7, X8))
qcG_in_ggggaa(X1, X2, X3, .(X4, X5), .(X4, X6), .(X7, X8)) → U54_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, gtcI_in_gg(X1, X2))
U54_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, gtcI_out_gg(X1, X2)) → U55_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, qcG_in_ggggaa(X1, X4, X3, X5, X6, X8))
U55_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, qcG_out_ggggaa(X1, X4, X3, X5, X6, X8)) → qcG_out_ggggaa(X1, X2, X3, .(X4, X5), .(X4, X6), .(X7, X8))
U49_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, qcG_out_ggggaa(X3, X2, X4, X5, X6, X8)) → qcF_out_ggggaa(X1, X2, .(X3, X4), X5, .(X2, X6), .(X7, X8))
U47_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, qcF_out_ggggaa(X3, X2, X4, X5, X6, X8)) → qcF_out_ggggaa(X1, X2, .(X3, X4), X5, .(X3, X6), .(X7, X8))
U42_ggaaa(X1, X2, X3, X4, X5, X6, X7, qcF_out_ggggaa(X1, X3, X2, X4, X5, X7)) → mergecC_out_ggaaa(.(X1, X2), .(X3, X4), .(X1, X5), X6, X7)
mergecC_in_ggaaa(.(X1, X2), .(X3, X4), .(X3, X5), X6, X7) → U43_ggaaa(X1, X2, X3, X4, X5, X6, X7, qcG_in_ggggaa(X1, X3, X2, X4, X5, X7))
U43_ggaaa(X1, X2, X3, X4, X5, X6, X7, qcG_out_ggggaa(X1, X3, X2, X4, X5, X7)) → mergecC_out_ggaaa(.(X1, X2), .(X3, X4), .(X3, X5), X6, X7)
U41_gaa(X1, X2, X3, X4, X5, X6, mergecC_out_ggaaa(X9, X10, X4, X5, X6)) → mergesortcE_out_gaa(.(X1, .(X2, X3)), X4, .(X5, X6))
U35_gaa(X1, X2, X3, X4, X5, X6, X9, mergesortcE_out_gaa(X7, X10, X6)) → U36_gaa(X1, X2, X3, X4, X5, X6, mergecC_in_ggaaa(X9, X10, X4, X5, X6))
U36_gaa(X1, X2, X3, X4, X5, X6, mergecC_out_ggaaa(X9, X10, X4, X5, X6)) → mergesortcB_out_gaa(.(X1, .(X2, X3)), X4, .(X5, X6))
PF_IN_GGGGAA(X1, X2, .(X3, X4), X5, .(X3, X6), .(X7, X8)) → U14_GGGGAA(X1, X2, X3, X4, X5, X6, X7, X8, lecH_in_gg(X1, X2))
U14_GGGGAA(X1, X2, X3, X4, X5, X6, X7, X8, lecH_out_gg(X1, X2)) → PF_IN_GGGGAA(X3, X2, X4, X5, X6, X8)
PF_IN_GGGGAA(X1, X2, .(X3, X4), X5, .(X2, X6), .(X7, X8)) → U16_GGGGAA(X1, X2, X3, X4, X5, X6, X7, X8, lecH_in_gg(X1, X2))
U16_GGGGAA(X1, X2, X3, X4, X5, X6, X7, X8, lecH_out_gg(X1, X2)) → PG_IN_GGGGAA(X3, X2, X4, X5, X6, X8)
PG_IN_GGGGAA(X1, X2, X3, .(X4, X5), .(X1, X6), .(X7, X8)) → U20_GGGGAA(X1, X2, X3, X4, X5, X6, X7, X8, gtcI_in_gg(X1, X2))
U20_GGGGAA(X1, X2, X3, X4, X5, X6, X7, X8, gtcI_out_gg(X1, X2)) → PF_IN_GGGGAA(X1, X4, X3, X5, X6, X8)
PG_IN_GGGGAA(X1, X2, X3, .(X4, X5), .(X4, X6), .(X7, X8)) → U22_GGGGAA(X1, X2, X3, X4, X5, X6, X7, X8, gtcI_in_gg(X1, X2))
U22_GGGGAA(X1, X2, X3, X4, X5, X6, X7, X8, gtcI_out_gg(X1, X2)) → PG_IN_GGGGAA(X1, X4, X3, X5, X6, X8)
lecH_in_gg(s(X1), s(X2)) → U44_gg(X1, X2, lecH_in_gg(X1, X2))
lecH_in_gg(0, s(0)) → lecH_out_gg(0, s(0))
lecH_in_gg(0, 0) → lecH_out_gg(0, 0)
gtcI_in_gg(s(X1), s(X2)) → U50_gg(X1, X2, gtcI_in_gg(X1, X2))
gtcI_in_gg(s(0), 0) → gtcI_out_gg(s(0), 0)
U44_gg(X1, X2, lecH_out_gg(X1, X2)) → lecH_out_gg(s(X1), s(X2))
U50_gg(X1, X2, gtcI_out_gg(X1, X2)) → gtcI_out_gg(s(X1), s(X2))
PF_IN_GGGGAA(X1, X2, .(X3, X4), X5) → U14_GGGGAA(X1, X2, X3, X4, X5, lecH_in_gg(X1, X2))
U14_GGGGAA(X1, X2, X3, X4, X5, lecH_out_gg(X1, X2)) → PF_IN_GGGGAA(X3, X2, X4, X5)
PF_IN_GGGGAA(X1, X2, .(X3, X4), X5) → U16_GGGGAA(X1, X2, X3, X4, X5, lecH_in_gg(X1, X2))
U16_GGGGAA(X1, X2, X3, X4, X5, lecH_out_gg(X1, X2)) → PG_IN_GGGGAA(X3, X2, X4, X5)
PG_IN_GGGGAA(X1, X2, X3, .(X4, X5)) → U20_GGGGAA(X1, X2, X3, X4, X5, gtcI_in_gg(X1, X2))
U20_GGGGAA(X1, X2, X3, X4, X5, gtcI_out_gg(X1, X2)) → PF_IN_GGGGAA(X1, X4, X3, X5)
PG_IN_GGGGAA(X1, X2, X3, .(X4, X5)) → U22_GGGGAA(X1, X2, X3, X4, X5, gtcI_in_gg(X1, X2))
U22_GGGGAA(X1, X2, X3, X4, X5, gtcI_out_gg(X1, X2)) → PG_IN_GGGGAA(X1, X4, X3, X5)
lecH_in_gg(s(X1), s(X2)) → U44_gg(X1, X2, lecH_in_gg(X1, X2))
lecH_in_gg(0, s(0)) → lecH_out_gg(0, s(0))
lecH_in_gg(0, 0) → lecH_out_gg(0, 0)
gtcI_in_gg(s(X1), s(X2)) → U50_gg(X1, X2, gtcI_in_gg(X1, X2))
gtcI_in_gg(s(0), 0) → gtcI_out_gg(s(0), 0)
U44_gg(X1, X2, lecH_out_gg(X1, X2)) → lecH_out_gg(s(X1), s(X2))
U50_gg(X1, X2, gtcI_out_gg(X1, X2)) → gtcI_out_gg(s(X1), s(X2))
lecH_in_gg(x0, x1)
gtcI_in_gg(x0, x1)
U44_gg(x0, x1, x2)
U50_gg(x0, x1, x2)
From the DPs we obtained the following set of size-change graphs:
SPLITA_IN_GAAA(.(X1, X2), .(X1, X3), X4, .(X5, X6)) → SPLITA_IN_GAAA(X2, X4, X3, X6)
splitcD_in_ggaaa(X1, X2, .(X1, X3), X4, .(X5, X6)) → U37_ggaaa(X1, X2, X3, X4, X5, X6, splitcA_in_gaaa(X2, X4, X3, X6))
splitcA_in_gaaa([], [], [], X1) → splitcA_out_gaaa([], [], [], X1)
splitcA_in_gaaa(.(X1, X2), .(X1, X3), X4, .(X5, X6)) → U32_gaaa(X1, X2, X3, X4, X5, X6, splitcA_in_gaaa(X2, X4, X3, X6))
U32_gaaa(X1, X2, X3, X4, X5, X6, splitcA_out_gaaa(X2, X4, X3, X6)) → splitcA_out_gaaa(.(X1, X2), .(X1, X3), X4, .(X5, X6))
U37_ggaaa(X1, X2, X3, X4, X5, X6, splitcA_out_gaaa(X2, X4, X3, X6)) → splitcD_out_ggaaa(X1, X2, .(X1, X3), X4, .(X5, X6))
mergesortcB_in_gaa([], [], X1) → mergesortcB_out_gaa([], [], X1)
mergesortcB_in_gaa(.(X1, []), .(X1, []), X2) → mergesortcB_out_gaa(.(X1, []), .(X1, []), X2)
mergesortcB_in_gaa(.(X1, .(X2, X3)), X4, .(X5, X6)) → U33_gaa(X1, X2, X3, X4, X5, X6, splitcD_in_ggaaa(X2, X3, X7, X8, X6))
U33_gaa(X1, X2, X3, X4, X5, X6, splitcD_out_ggaaa(X2, X3, X7, X8, X6)) → U34_gaa(X1, X2, X3, X4, X5, X6, X7, mergesortcB_in_gaa(.(X1, X8), X9, X6))
U34_gaa(X1, X2, X3, X4, X5, X6, X7, mergesortcB_out_gaa(.(X1, X8), X9, X6)) → U35_gaa(X1, X2, X3, X4, X5, X6, X9, mergesortcE_in_gaa(X7, X10, X6))
mergesortcE_in_gaa([], [], X1) → mergesortcE_out_gaa([], [], X1)
mergesortcE_in_gaa(.(X1, []), .(X1, []), X2) → mergesortcE_out_gaa(.(X1, []), .(X1, []), X2)
mergesortcE_in_gaa(.(X1, .(X2, X3)), X4, .(X5, X6)) → U38_gaa(X1, X2, X3, X4, X5, X6, splitcD_in_ggaaa(X1, .(X2, X3), X7, X8, .(X5, X6)))
U38_gaa(X1, X2, X3, X4, X5, X6, splitcD_out_ggaaa(X1, .(X2, X3), X7, X8, .(X5, X6))) → U39_gaa(X1, X2, X3, X4, X5, X6, X8, mergesortcE_in_gaa(X7, X9, X6))
U39_gaa(X1, X2, X3, X4, X5, X6, X8, mergesortcE_out_gaa(X7, X9, X6)) → U40_gaa(X1, X2, X3, X4, X5, X6, X9, mergesortcE_in_gaa(X8, X10, X6))
U40_gaa(X1, X2, X3, X4, X5, X6, X9, mergesortcE_out_gaa(X8, X10, X6)) → U41_gaa(X1, X2, X3, X4, X5, X6, mergecC_in_ggaaa(X9, X10, X4, X5, X6))
mergecC_in_ggaaa([], X1, X1, X2, X3) → mergecC_out_ggaaa([], X1, X1, X2, X3)
mergecC_in_ggaaa(X1, [], X1, X2, X3) → mergecC_out_ggaaa(X1, [], X1, X2, X3)
mergecC_in_ggaaa(.(X1, X2), .(X3, X4), .(X1, X5), X6, X7) → U42_ggaaa(X1, X2, X3, X4, X5, X6, X7, qcF_in_ggggaa(X1, X3, X2, X4, X5, X7))
qcF_in_ggggaa(X1, X2, [], X3, .(X2, X3), X4) → U45_ggggaa(X1, X2, X3, X4, lecH_in_gg(X1, X2))
lecH_in_gg(s(X1), s(X2)) → U44_gg(X1, X2, lecH_in_gg(X1, X2))
lecH_in_gg(0, s(0)) → lecH_out_gg(0, s(0))
lecH_in_gg(0, 0) → lecH_out_gg(0, 0)
U44_gg(X1, X2, lecH_out_gg(X1, X2)) → lecH_out_gg(s(X1), s(X2))
U45_ggggaa(X1, X2, X3, X4, lecH_out_gg(X1, X2)) → qcF_out_ggggaa(X1, X2, [], X3, .(X2, X3), X4)
qcF_in_ggggaa(X1, X2, .(X3, X4), X5, .(X3, X6), .(X7, X8)) → U46_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, lecH_in_gg(X1, X2))
U46_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, lecH_out_gg(X1, X2)) → U47_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, qcF_in_ggggaa(X3, X2, X4, X5, X6, X8))
qcF_in_ggggaa(X1, X2, .(X3, X4), X5, .(X2, X6), .(X7, X8)) → U48_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, lecH_in_gg(X1, X2))
U48_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, lecH_out_gg(X1, X2)) → U49_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, qcG_in_ggggaa(X3, X2, X4, X5, X6, X8))
qcG_in_ggggaa(X1, X2, X3, [], .(X1, X3), X4) → U51_ggggaa(X1, X2, X3, X4, gtcI_in_gg(X1, X2))
gtcI_in_gg(s(X1), s(X2)) → U50_gg(X1, X2, gtcI_in_gg(X1, X2))
gtcI_in_gg(s(0), 0) → gtcI_out_gg(s(0), 0)
U50_gg(X1, X2, gtcI_out_gg(X1, X2)) → gtcI_out_gg(s(X1), s(X2))
U51_ggggaa(X1, X2, X3, X4, gtcI_out_gg(X1, X2)) → qcG_out_ggggaa(X1, X2, X3, [], .(X1, X3), X4)
qcG_in_ggggaa(X1, X2, X3, .(X4, X5), .(X1, X6), .(X7, X8)) → U52_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, gtcI_in_gg(X1, X2))
U52_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, gtcI_out_gg(X1, X2)) → U53_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, qcF_in_ggggaa(X1, X4, X3, X5, X6, X8))
U53_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, qcF_out_ggggaa(X1, X4, X3, X5, X6, X8)) → qcG_out_ggggaa(X1, X2, X3, .(X4, X5), .(X1, X6), .(X7, X8))
qcG_in_ggggaa(X1, X2, X3, .(X4, X5), .(X4, X6), .(X7, X8)) → U54_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, gtcI_in_gg(X1, X2))
U54_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, gtcI_out_gg(X1, X2)) → U55_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, qcG_in_ggggaa(X1, X4, X3, X5, X6, X8))
U55_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, qcG_out_ggggaa(X1, X4, X3, X5, X6, X8)) → qcG_out_ggggaa(X1, X2, X3, .(X4, X5), .(X4, X6), .(X7, X8))
U49_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, qcG_out_ggggaa(X3, X2, X4, X5, X6, X8)) → qcF_out_ggggaa(X1, X2, .(X3, X4), X5, .(X2, X6), .(X7, X8))
U47_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, qcF_out_ggggaa(X3, X2, X4, X5, X6, X8)) → qcF_out_ggggaa(X1, X2, .(X3, X4), X5, .(X3, X6), .(X7, X8))
U42_ggaaa(X1, X2, X3, X4, X5, X6, X7, qcF_out_ggggaa(X1, X3, X2, X4, X5, X7)) → mergecC_out_ggaaa(.(X1, X2), .(X3, X4), .(X1, X5), X6, X7)
mergecC_in_ggaaa(.(X1, X2), .(X3, X4), .(X3, X5), X6, X7) → U43_ggaaa(X1, X2, X3, X4, X5, X6, X7, qcG_in_ggggaa(X1, X3, X2, X4, X5, X7))
U43_ggaaa(X1, X2, X3, X4, X5, X6, X7, qcG_out_ggggaa(X1, X3, X2, X4, X5, X7)) → mergecC_out_ggaaa(.(X1, X2), .(X3, X4), .(X3, X5), X6, X7)
U41_gaa(X1, X2, X3, X4, X5, X6, mergecC_out_ggaaa(X9, X10, X4, X5, X6)) → mergesortcE_out_gaa(.(X1, .(X2, X3)), X4, .(X5, X6))
U35_gaa(X1, X2, X3, X4, X5, X6, X9, mergesortcE_out_gaa(X7, X10, X6)) → U36_gaa(X1, X2, X3, X4, X5, X6, mergecC_in_ggaaa(X9, X10, X4, X5, X6))
U36_gaa(X1, X2, X3, X4, X5, X6, mergecC_out_ggaaa(X9, X10, X4, X5, X6)) → mergesortcB_out_gaa(.(X1, .(X2, X3)), X4, .(X5, X6))
SPLITA_IN_GAAA(.(X1, X2), .(X1, X3), X4, .(X5, X6)) → SPLITA_IN_GAAA(X2, X4, X3, X6)
SPLITA_IN_GAAA(.(X1, X2)) → SPLITA_IN_GAAA(X2)
From the DPs we obtained the following set of size-change graphs:
MERGESORTE_IN_GAA(.(X1, .(X2, X3)), X4, .(X5, X6)) → U4_GAA(X1, X2, X3, X4, X5, X6, splitcD_in_ggaaa(X1, .(X2, X3), X7, X8, .(X5, X6)))
U4_GAA(X1, X2, X3, X4, X5, X6, splitcD_out_ggaaa(X1, .(X2, X3), X7, X8, .(X5, X6))) → MERGESORTE_IN_GAA(X7, X9, X6)
U4_GAA(X1, X2, X3, X4, X5, X6, splitcD_out_ggaaa(X1, .(X2, X3), X7, X8, .(X5, X6))) → U6_GAA(X1, X2, X3, X4, X5, X6, X8, mergesortcE_in_gaa(X7, X9, X6))
U6_GAA(X1, X2, X3, X4, X5, X6, X8, mergesortcE_out_gaa(X7, X9, X6)) → MERGESORTE_IN_GAA(X8, X10, X6)
splitcD_in_ggaaa(X1, X2, .(X1, X3), X4, .(X5, X6)) → U37_ggaaa(X1, X2, X3, X4, X5, X6, splitcA_in_gaaa(X2, X4, X3, X6))
splitcA_in_gaaa([], [], [], X1) → splitcA_out_gaaa([], [], [], X1)
splitcA_in_gaaa(.(X1, X2), .(X1, X3), X4, .(X5, X6)) → U32_gaaa(X1, X2, X3, X4, X5, X6, splitcA_in_gaaa(X2, X4, X3, X6))
U32_gaaa(X1, X2, X3, X4, X5, X6, splitcA_out_gaaa(X2, X4, X3, X6)) → splitcA_out_gaaa(.(X1, X2), .(X1, X3), X4, .(X5, X6))
U37_ggaaa(X1, X2, X3, X4, X5, X6, splitcA_out_gaaa(X2, X4, X3, X6)) → splitcD_out_ggaaa(X1, X2, .(X1, X3), X4, .(X5, X6))
mergesortcB_in_gaa([], [], X1) → mergesortcB_out_gaa([], [], X1)
mergesortcB_in_gaa(.(X1, []), .(X1, []), X2) → mergesortcB_out_gaa(.(X1, []), .(X1, []), X2)
mergesortcB_in_gaa(.(X1, .(X2, X3)), X4, .(X5, X6)) → U33_gaa(X1, X2, X3, X4, X5, X6, splitcD_in_ggaaa(X2, X3, X7, X8, X6))
U33_gaa(X1, X2, X3, X4, X5, X6, splitcD_out_ggaaa(X2, X3, X7, X8, X6)) → U34_gaa(X1, X2, X3, X4, X5, X6, X7, mergesortcB_in_gaa(.(X1, X8), X9, X6))
U34_gaa(X1, X2, X3, X4, X5, X6, X7, mergesortcB_out_gaa(.(X1, X8), X9, X6)) → U35_gaa(X1, X2, X3, X4, X5, X6, X9, mergesortcE_in_gaa(X7, X10, X6))
mergesortcE_in_gaa([], [], X1) → mergesortcE_out_gaa([], [], X1)
mergesortcE_in_gaa(.(X1, []), .(X1, []), X2) → mergesortcE_out_gaa(.(X1, []), .(X1, []), X2)
mergesortcE_in_gaa(.(X1, .(X2, X3)), X4, .(X5, X6)) → U38_gaa(X1, X2, X3, X4, X5, X6, splitcD_in_ggaaa(X1, .(X2, X3), X7, X8, .(X5, X6)))
U38_gaa(X1, X2, X3, X4, X5, X6, splitcD_out_ggaaa(X1, .(X2, X3), X7, X8, .(X5, X6))) → U39_gaa(X1, X2, X3, X4, X5, X6, X8, mergesortcE_in_gaa(X7, X9, X6))
U39_gaa(X1, X2, X3, X4, X5, X6, X8, mergesortcE_out_gaa(X7, X9, X6)) → U40_gaa(X1, X2, X3, X4, X5, X6, X9, mergesortcE_in_gaa(X8, X10, X6))
U40_gaa(X1, X2, X3, X4, X5, X6, X9, mergesortcE_out_gaa(X8, X10, X6)) → U41_gaa(X1, X2, X3, X4, X5, X6, mergecC_in_ggaaa(X9, X10, X4, X5, X6))
mergecC_in_ggaaa([], X1, X1, X2, X3) → mergecC_out_ggaaa([], X1, X1, X2, X3)
mergecC_in_ggaaa(X1, [], X1, X2, X3) → mergecC_out_ggaaa(X1, [], X1, X2, X3)
mergecC_in_ggaaa(.(X1, X2), .(X3, X4), .(X1, X5), X6, X7) → U42_ggaaa(X1, X2, X3, X4, X5, X6, X7, qcF_in_ggggaa(X1, X3, X2, X4, X5, X7))
qcF_in_ggggaa(X1, X2, [], X3, .(X2, X3), X4) → U45_ggggaa(X1, X2, X3, X4, lecH_in_gg(X1, X2))
lecH_in_gg(s(X1), s(X2)) → U44_gg(X1, X2, lecH_in_gg(X1, X2))
lecH_in_gg(0, s(0)) → lecH_out_gg(0, s(0))
lecH_in_gg(0, 0) → lecH_out_gg(0, 0)
U44_gg(X1, X2, lecH_out_gg(X1, X2)) → lecH_out_gg(s(X1), s(X2))
U45_ggggaa(X1, X2, X3, X4, lecH_out_gg(X1, X2)) → qcF_out_ggggaa(X1, X2, [], X3, .(X2, X3), X4)
qcF_in_ggggaa(X1, X2, .(X3, X4), X5, .(X3, X6), .(X7, X8)) → U46_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, lecH_in_gg(X1, X2))
U46_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, lecH_out_gg(X1, X2)) → U47_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, qcF_in_ggggaa(X3, X2, X4, X5, X6, X8))
qcF_in_ggggaa(X1, X2, .(X3, X4), X5, .(X2, X6), .(X7, X8)) → U48_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, lecH_in_gg(X1, X2))
U48_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, lecH_out_gg(X1, X2)) → U49_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, qcG_in_ggggaa(X3, X2, X4, X5, X6, X8))
qcG_in_ggggaa(X1, X2, X3, [], .(X1, X3), X4) → U51_ggggaa(X1, X2, X3, X4, gtcI_in_gg(X1, X2))
gtcI_in_gg(s(X1), s(X2)) → U50_gg(X1, X2, gtcI_in_gg(X1, X2))
gtcI_in_gg(s(0), 0) → gtcI_out_gg(s(0), 0)
U50_gg(X1, X2, gtcI_out_gg(X1, X2)) → gtcI_out_gg(s(X1), s(X2))
U51_ggggaa(X1, X2, X3, X4, gtcI_out_gg(X1, X2)) → qcG_out_ggggaa(X1, X2, X3, [], .(X1, X3), X4)
qcG_in_ggggaa(X1, X2, X3, .(X4, X5), .(X1, X6), .(X7, X8)) → U52_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, gtcI_in_gg(X1, X2))
U52_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, gtcI_out_gg(X1, X2)) → U53_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, qcF_in_ggggaa(X1, X4, X3, X5, X6, X8))
U53_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, qcF_out_ggggaa(X1, X4, X3, X5, X6, X8)) → qcG_out_ggggaa(X1, X2, X3, .(X4, X5), .(X1, X6), .(X7, X8))
qcG_in_ggggaa(X1, X2, X3, .(X4, X5), .(X4, X6), .(X7, X8)) → U54_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, gtcI_in_gg(X1, X2))
U54_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, gtcI_out_gg(X1, X2)) → U55_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, qcG_in_ggggaa(X1, X4, X3, X5, X6, X8))
U55_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, qcG_out_ggggaa(X1, X4, X3, X5, X6, X8)) → qcG_out_ggggaa(X1, X2, X3, .(X4, X5), .(X4, X6), .(X7, X8))
U49_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, qcG_out_ggggaa(X3, X2, X4, X5, X6, X8)) → qcF_out_ggggaa(X1, X2, .(X3, X4), X5, .(X2, X6), .(X7, X8))
U47_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, qcF_out_ggggaa(X3, X2, X4, X5, X6, X8)) → qcF_out_ggggaa(X1, X2, .(X3, X4), X5, .(X3, X6), .(X7, X8))
U42_ggaaa(X1, X2, X3, X4, X5, X6, X7, qcF_out_ggggaa(X1, X3, X2, X4, X5, X7)) → mergecC_out_ggaaa(.(X1, X2), .(X3, X4), .(X1, X5), X6, X7)
mergecC_in_ggaaa(.(X1, X2), .(X3, X4), .(X3, X5), X6, X7) → U43_ggaaa(X1, X2, X3, X4, X5, X6, X7, qcG_in_ggggaa(X1, X3, X2, X4, X5, X7))
U43_ggaaa(X1, X2, X3, X4, X5, X6, X7, qcG_out_ggggaa(X1, X3, X2, X4, X5, X7)) → mergecC_out_ggaaa(.(X1, X2), .(X3, X4), .(X3, X5), X6, X7)
U41_gaa(X1, X2, X3, X4, X5, X6, mergecC_out_ggaaa(X9, X10, X4, X5, X6)) → mergesortcE_out_gaa(.(X1, .(X2, X3)), X4, .(X5, X6))
U35_gaa(X1, X2, X3, X4, X5, X6, X9, mergesortcE_out_gaa(X7, X10, X6)) → U36_gaa(X1, X2, X3, X4, X5, X6, mergecC_in_ggaaa(X9, X10, X4, X5, X6))
U36_gaa(X1, X2, X3, X4, X5, X6, mergecC_out_ggaaa(X9, X10, X4, X5, X6)) → mergesortcB_out_gaa(.(X1, .(X2, X3)), X4, .(X5, X6))
MERGESORTE_IN_GAA(.(X1, .(X2, X3)), X4, .(X5, X6)) → U4_GAA(X1, X2, X3, X4, X5, X6, splitcD_in_ggaaa(X1, .(X2, X3), X7, X8, .(X5, X6)))
U4_GAA(X1, X2, X3, X4, X5, X6, splitcD_out_ggaaa(X1, .(X2, X3), X7, X8, .(X5, X6))) → MERGESORTE_IN_GAA(X7, X9, X6)
U4_GAA(X1, X2, X3, X4, X5, X6, splitcD_out_ggaaa(X1, .(X2, X3), X7, X8, .(X5, X6))) → U6_GAA(X1, X2, X3, X4, X5, X6, X8, mergesortcE_in_gaa(X7, X9, X6))
U6_GAA(X1, X2, X3, X4, X5, X6, X8, mergesortcE_out_gaa(X7, X9, X6)) → MERGESORTE_IN_GAA(X8, X10, X6)
splitcD_in_ggaaa(X1, X2, .(X1, X3), X4, .(X5, X6)) → U37_ggaaa(X1, X2, X3, X4, X5, X6, splitcA_in_gaaa(X2, X4, X3, X6))
mergesortcE_in_gaa([], [], X1) → mergesortcE_out_gaa([], [], X1)
mergesortcE_in_gaa(.(X1, []), .(X1, []), X2) → mergesortcE_out_gaa(.(X1, []), .(X1, []), X2)
mergesortcE_in_gaa(.(X1, .(X2, X3)), X4, .(X5, X6)) → U38_gaa(X1, X2, X3, X4, X5, X6, splitcD_in_ggaaa(X1, .(X2, X3), X7, X8, .(X5, X6)))
U37_ggaaa(X1, X2, X3, X4, X5, X6, splitcA_out_gaaa(X2, X4, X3, X6)) → splitcD_out_ggaaa(X1, X2, .(X1, X3), X4, .(X5, X6))
U38_gaa(X1, X2, X3, X4, X5, X6, splitcD_out_ggaaa(X1, .(X2, X3), X7, X8, .(X5, X6))) → U39_gaa(X1, X2, X3, X4, X5, X6, X8, mergesortcE_in_gaa(X7, X9, X6))
splitcA_in_gaaa([], [], [], X1) → splitcA_out_gaaa([], [], [], X1)
splitcA_in_gaaa(.(X1, X2), .(X1, X3), X4, .(X5, X6)) → U32_gaaa(X1, X2, X3, X4, X5, X6, splitcA_in_gaaa(X2, X4, X3, X6))
U39_gaa(X1, X2, X3, X4, X5, X6, X8, mergesortcE_out_gaa(X7, X9, X6)) → U40_gaa(X1, X2, X3, X4, X5, X6, X9, mergesortcE_in_gaa(X8, X10, X6))
U32_gaaa(X1, X2, X3, X4, X5, X6, splitcA_out_gaaa(X2, X4, X3, X6)) → splitcA_out_gaaa(.(X1, X2), .(X1, X3), X4, .(X5, X6))
U40_gaa(X1, X2, X3, X4, X5, X6, X9, mergesortcE_out_gaa(X8, X10, X6)) → U41_gaa(X1, X2, X3, X4, X5, X6, mergecC_in_ggaaa(X9, X10, X4, X5, X6))
U41_gaa(X1, X2, X3, X4, X5, X6, mergecC_out_ggaaa(X9, X10, X4, X5, X6)) → mergesortcE_out_gaa(.(X1, .(X2, X3)), X4, .(X5, X6))
mergecC_in_ggaaa([], X1, X1, X2, X3) → mergecC_out_ggaaa([], X1, X1, X2, X3)
mergecC_in_ggaaa(X1, [], X1, X2, X3) → mergecC_out_ggaaa(X1, [], X1, X2, X3)
mergecC_in_ggaaa(.(X1, X2), .(X3, X4), .(X1, X5), X6, X7) → U42_ggaaa(X1, X2, X3, X4, X5, X6, X7, qcF_in_ggggaa(X1, X3, X2, X4, X5, X7))
mergecC_in_ggaaa(.(X1, X2), .(X3, X4), .(X3, X5), X6, X7) → U43_ggaaa(X1, X2, X3, X4, X5, X6, X7, qcG_in_ggggaa(X1, X3, X2, X4, X5, X7))
U42_ggaaa(X1, X2, X3, X4, X5, X6, X7, qcF_out_ggggaa(X1, X3, X2, X4, X5, X7)) → mergecC_out_ggaaa(.(X1, X2), .(X3, X4), .(X1, X5), X6, X7)
U43_ggaaa(X1, X2, X3, X4, X5, X6, X7, qcG_out_ggggaa(X1, X3, X2, X4, X5, X7)) → mergecC_out_ggaaa(.(X1, X2), .(X3, X4), .(X3, X5), X6, X7)
qcF_in_ggggaa(X1, X2, [], X3, .(X2, X3), X4) → U45_ggggaa(X1, X2, X3, X4, lecH_in_gg(X1, X2))
qcF_in_ggggaa(X1, X2, .(X3, X4), X5, .(X3, X6), .(X7, X8)) → U46_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, lecH_in_gg(X1, X2))
qcF_in_ggggaa(X1, X2, .(X3, X4), X5, .(X2, X6), .(X7, X8)) → U48_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, lecH_in_gg(X1, X2))
qcG_in_ggggaa(X1, X2, X3, [], .(X1, X3), X4) → U51_ggggaa(X1, X2, X3, X4, gtcI_in_gg(X1, X2))
qcG_in_ggggaa(X1, X2, X3, .(X4, X5), .(X1, X6), .(X7, X8)) → U52_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, gtcI_in_gg(X1, X2))
qcG_in_ggggaa(X1, X2, X3, .(X4, X5), .(X4, X6), .(X7, X8)) → U54_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, gtcI_in_gg(X1, X2))
U45_ggggaa(X1, X2, X3, X4, lecH_out_gg(X1, X2)) → qcF_out_ggggaa(X1, X2, [], X3, .(X2, X3), X4)
U46_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, lecH_out_gg(X1, X2)) → U47_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, qcF_in_ggggaa(X3, X2, X4, X5, X6, X8))
U48_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, lecH_out_gg(X1, X2)) → U49_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, qcG_in_ggggaa(X3, X2, X4, X5, X6, X8))
U51_ggggaa(X1, X2, X3, X4, gtcI_out_gg(X1, X2)) → qcG_out_ggggaa(X1, X2, X3, [], .(X1, X3), X4)
U52_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, gtcI_out_gg(X1, X2)) → U53_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, qcF_in_ggggaa(X1, X4, X3, X5, X6, X8))
U54_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, gtcI_out_gg(X1, X2)) → U55_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, qcG_in_ggggaa(X1, X4, X3, X5, X6, X8))
lecH_in_gg(s(X1), s(X2)) → U44_gg(X1, X2, lecH_in_gg(X1, X2))
lecH_in_gg(0, s(0)) → lecH_out_gg(0, s(0))
lecH_in_gg(0, 0) → lecH_out_gg(0, 0)
U47_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, qcF_out_ggggaa(X3, X2, X4, X5, X6, X8)) → qcF_out_ggggaa(X1, X2, .(X3, X4), X5, .(X3, X6), .(X7, X8))
U49_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, qcG_out_ggggaa(X3, X2, X4, X5, X6, X8)) → qcF_out_ggggaa(X1, X2, .(X3, X4), X5, .(X2, X6), .(X7, X8))
gtcI_in_gg(s(X1), s(X2)) → U50_gg(X1, X2, gtcI_in_gg(X1, X2))
gtcI_in_gg(s(0), 0) → gtcI_out_gg(s(0), 0)
U53_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, qcF_out_ggggaa(X1, X4, X3, X5, X6, X8)) → qcG_out_ggggaa(X1, X2, X3, .(X4, X5), .(X1, X6), .(X7, X8))
U55_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, qcG_out_ggggaa(X1, X4, X3, X5, X6, X8)) → qcG_out_ggggaa(X1, X2, X3, .(X4, X5), .(X4, X6), .(X7, X8))
U44_gg(X1, X2, lecH_out_gg(X1, X2)) → lecH_out_gg(s(X1), s(X2))
U50_gg(X1, X2, gtcI_out_gg(X1, X2)) → gtcI_out_gg(s(X1), s(X2))
MERGESORTE_IN_GAA(.(X1, .(X2, X3))) → U4_GAA(X1, X2, X3, splitcD_in_ggaaa(X1, .(X2, X3)))
U4_GAA(X1, X2, X3, splitcD_out_ggaaa(X1, .(X2, X3), X7, X8)) → MERGESORTE_IN_GAA(X7)
U4_GAA(X1, X2, X3, splitcD_out_ggaaa(X1, .(X2, X3), X7, X8)) → U6_GAA(X1, X2, X3, X8, mergesortcE_in_gaa(X7))
U6_GAA(X1, X2, X3, X8, mergesortcE_out_gaa(X7, X9)) → MERGESORTE_IN_GAA(X8)
splitcD_in_ggaaa(X1, X2) → U37_ggaaa(X1, X2, splitcA_in_gaaa(X2))
mergesortcE_in_gaa([]) → mergesortcE_out_gaa([], [])
mergesortcE_in_gaa(.(X1, [])) → mergesortcE_out_gaa(.(X1, []), .(X1, []))
mergesortcE_in_gaa(.(X1, .(X2, X3))) → U38_gaa(X1, X2, X3, splitcD_in_ggaaa(X1, .(X2, X3)))
U37_ggaaa(X1, X2, splitcA_out_gaaa(X2, X4, X3)) → splitcD_out_ggaaa(X1, X2, .(X1, X3), X4)
U38_gaa(X1, X2, X3, splitcD_out_ggaaa(X1, .(X2, X3), X7, X8)) → U39_gaa(X1, X2, X3, X8, mergesortcE_in_gaa(X7))
splitcA_in_gaaa([]) → splitcA_out_gaaa([], [], [])
splitcA_in_gaaa(.(X1, X2)) → U32_gaaa(X1, X2, splitcA_in_gaaa(X2))
U39_gaa(X1, X2, X3, X8, mergesortcE_out_gaa(X7, X9)) → U40_gaa(X1, X2, X3, X9, mergesortcE_in_gaa(X8))
U32_gaaa(X1, X2, splitcA_out_gaaa(X2, X4, X3)) → splitcA_out_gaaa(.(X1, X2), .(X1, X3), X4)
U40_gaa(X1, X2, X3, X9, mergesortcE_out_gaa(X8, X10)) → U41_gaa(X1, X2, X3, mergecC_in_ggaaa(X9, X10))
U41_gaa(X1, X2, X3, mergecC_out_ggaaa(X9, X10, X4)) → mergesortcE_out_gaa(.(X1, .(X2, X3)), X4)
mergecC_in_ggaaa([], X1) → mergecC_out_ggaaa([], X1, X1)
mergecC_in_ggaaa(X1, []) → mergecC_out_ggaaa(X1, [], X1)
mergecC_in_ggaaa(.(X1, X2), .(X3, X4)) → U42_ggaaa(X1, X2, X3, X4, qcF_in_ggggaa(X1, X3, X2, X4))
mergecC_in_ggaaa(.(X1, X2), .(X3, X4)) → U43_ggaaa(X1, X2, X3, X4, qcG_in_ggggaa(X1, X3, X2, X4))
U42_ggaaa(X1, X2, X3, X4, qcF_out_ggggaa(X1, X3, X2, X4, X5)) → mergecC_out_ggaaa(.(X1, X2), .(X3, X4), .(X1, X5))
U43_ggaaa(X1, X2, X3, X4, qcG_out_ggggaa(X1, X3, X2, X4, X5)) → mergecC_out_ggaaa(.(X1, X2), .(X3, X4), .(X3, X5))
qcF_in_ggggaa(X1, X2, [], X3) → U45_ggggaa(X1, X2, X3, lecH_in_gg(X1, X2))
qcF_in_ggggaa(X1, X2, .(X3, X4), X5) → U46_ggggaa(X1, X2, X3, X4, X5, lecH_in_gg(X1, X2))
qcF_in_ggggaa(X1, X2, .(X3, X4), X5) → U48_ggggaa(X1, X2, X3, X4, X5, lecH_in_gg(X1, X2))
qcG_in_ggggaa(X1, X2, X3, []) → U51_ggggaa(X1, X2, X3, gtcI_in_gg(X1, X2))
qcG_in_ggggaa(X1, X2, X3, .(X4, X5)) → U52_ggggaa(X1, X2, X3, X4, X5, gtcI_in_gg(X1, X2))
qcG_in_ggggaa(X1, X2, X3, .(X4, X5)) → U54_ggggaa(X1, X2, X3, X4, X5, gtcI_in_gg(X1, X2))
U45_ggggaa(X1, X2, X3, lecH_out_gg(X1, X2)) → qcF_out_ggggaa(X1, X2, [], X3, .(X2, X3))
U46_ggggaa(X1, X2, X3, X4, X5, lecH_out_gg(X1, X2)) → U47_ggggaa(X1, X2, X3, X4, X5, qcF_in_ggggaa(X3, X2, X4, X5))
U48_ggggaa(X1, X2, X3, X4, X5, lecH_out_gg(X1, X2)) → U49_ggggaa(X1, X2, X3, X4, X5, qcG_in_ggggaa(X3, X2, X4, X5))
U51_ggggaa(X1, X2, X3, gtcI_out_gg(X1, X2)) → qcG_out_ggggaa(X1, X2, X3, [], .(X1, X3))
U52_ggggaa(X1, X2, X3, X4, X5, gtcI_out_gg(X1, X2)) → U53_ggggaa(X1, X2, X3, X4, X5, qcF_in_ggggaa(X1, X4, X3, X5))
U54_ggggaa(X1, X2, X3, X4, X5, gtcI_out_gg(X1, X2)) → U55_ggggaa(X1, X2, X3, X4, X5, qcG_in_ggggaa(X1, X4, X3, X5))
lecH_in_gg(s(X1), s(X2)) → U44_gg(X1, X2, lecH_in_gg(X1, X2))
lecH_in_gg(0, s(0)) → lecH_out_gg(0, s(0))
lecH_in_gg(0, 0) → lecH_out_gg(0, 0)
U47_ggggaa(X1, X2, X3, X4, X5, qcF_out_ggggaa(X3, X2, X4, X5, X6)) → qcF_out_ggggaa(X1, X2, .(X3, X4), X5, .(X3, X6))
U49_ggggaa(X1, X2, X3, X4, X5, qcG_out_ggggaa(X3, X2, X4, X5, X6)) → qcF_out_ggggaa(X1, X2, .(X3, X4), X5, .(X2, X6))
gtcI_in_gg(s(X1), s(X2)) → U50_gg(X1, X2, gtcI_in_gg(X1, X2))
gtcI_in_gg(s(0), 0) → gtcI_out_gg(s(0), 0)
U53_ggggaa(X1, X2, X3, X4, X5, qcF_out_ggggaa(X1, X4, X3, X5, X6)) → qcG_out_ggggaa(X1, X2, X3, .(X4, X5), .(X1, X6))
U55_ggggaa(X1, X2, X3, X4, X5, qcG_out_ggggaa(X1, X4, X3, X5, X6)) → qcG_out_ggggaa(X1, X2, X3, .(X4, X5), .(X4, X6))
U44_gg(X1, X2, lecH_out_gg(X1, X2)) → lecH_out_gg(s(X1), s(X2))
U50_gg(X1, X2, gtcI_out_gg(X1, X2)) → gtcI_out_gg(s(X1), s(X2))
splitcD_in_ggaaa(x0, x1)
mergesortcE_in_gaa(x0)
U37_ggaaa(x0, x1, x2)
U38_gaa(x0, x1, x2, x3)
splitcA_in_gaaa(x0)
U39_gaa(x0, x1, x2, x3, x4)
U32_gaaa(x0, x1, x2)
U40_gaa(x0, x1, x2, x3, x4)
U41_gaa(x0, x1, x2, x3)
mergecC_in_ggaaa(x0, x1)
U42_ggaaa(x0, x1, x2, x3, x4)
U43_ggaaa(x0, x1, x2, x3, x4)
qcF_in_ggggaa(x0, x1, x2, x3)
qcG_in_ggggaa(x0, x1, x2, x3)
U45_ggggaa(x0, x1, x2, x3)
U46_ggggaa(x0, x1, x2, x3, x4, x5)
U48_ggggaa(x0, x1, x2, x3, x4, x5)
U51_ggggaa(x0, x1, x2, x3)
U52_ggggaa(x0, x1, x2, x3, x4, x5)
U54_ggggaa(x0, x1, x2, x3, x4, x5)
lecH_in_gg(x0, x1)
U47_ggggaa(x0, x1, x2, x3, x4, x5)
U49_ggggaa(x0, x1, x2, x3, x4, x5)
gtcI_in_gg(x0, x1)
U53_ggggaa(x0, x1, x2, x3, x4, x5)
U55_ggggaa(x0, x1, x2, x3, x4, x5)
U44_gg(x0, x1, x2)
U50_gg(x0, x1, x2)
MERGESORTE_IN_GAA(.(X1, .(X2, X3))) → U4_GAA(X1, X2, X3, U37_ggaaa(X1, .(X2, X3), splitcA_in_gaaa(.(X2, X3))))
U4_GAA(X1, X2, X3, splitcD_out_ggaaa(X1, .(X2, X3), X7, X8)) → MERGESORTE_IN_GAA(X7)
U4_GAA(X1, X2, X3, splitcD_out_ggaaa(X1, .(X2, X3), X7, X8)) → U6_GAA(X1, X2, X3, X8, mergesortcE_in_gaa(X7))
U6_GAA(X1, X2, X3, X8, mergesortcE_out_gaa(X7, X9)) → MERGESORTE_IN_GAA(X8)
MERGESORTE_IN_GAA(.(X1, .(X2, X3))) → U4_GAA(X1, X2, X3, U37_ggaaa(X1, .(X2, X3), splitcA_in_gaaa(.(X2, X3))))
splitcD_in_ggaaa(X1, X2) → U37_ggaaa(X1, X2, splitcA_in_gaaa(X2))
mergesortcE_in_gaa([]) → mergesortcE_out_gaa([], [])
mergesortcE_in_gaa(.(X1, [])) → mergesortcE_out_gaa(.(X1, []), .(X1, []))
mergesortcE_in_gaa(.(X1, .(X2, X3))) → U38_gaa(X1, X2, X3, splitcD_in_ggaaa(X1, .(X2, X3)))
U37_ggaaa(X1, X2, splitcA_out_gaaa(X2, X4, X3)) → splitcD_out_ggaaa(X1, X2, .(X1, X3), X4)
U38_gaa(X1, X2, X3, splitcD_out_ggaaa(X1, .(X2, X3), X7, X8)) → U39_gaa(X1, X2, X3, X8, mergesortcE_in_gaa(X7))
splitcA_in_gaaa([]) → splitcA_out_gaaa([], [], [])
splitcA_in_gaaa(.(X1, X2)) → U32_gaaa(X1, X2, splitcA_in_gaaa(X2))
U39_gaa(X1, X2, X3, X8, mergesortcE_out_gaa(X7, X9)) → U40_gaa(X1, X2, X3, X9, mergesortcE_in_gaa(X8))
U32_gaaa(X1, X2, splitcA_out_gaaa(X2, X4, X3)) → splitcA_out_gaaa(.(X1, X2), .(X1, X3), X4)
U40_gaa(X1, X2, X3, X9, mergesortcE_out_gaa(X8, X10)) → U41_gaa(X1, X2, X3, mergecC_in_ggaaa(X9, X10))
U41_gaa(X1, X2, X3, mergecC_out_ggaaa(X9, X10, X4)) → mergesortcE_out_gaa(.(X1, .(X2, X3)), X4)
mergecC_in_ggaaa([], X1) → mergecC_out_ggaaa([], X1, X1)
mergecC_in_ggaaa(X1, []) → mergecC_out_ggaaa(X1, [], X1)
mergecC_in_ggaaa(.(X1, X2), .(X3, X4)) → U42_ggaaa(X1, X2, X3, X4, qcF_in_ggggaa(X1, X3, X2, X4))
mergecC_in_ggaaa(.(X1, X2), .(X3, X4)) → U43_ggaaa(X1, X2, X3, X4, qcG_in_ggggaa(X1, X3, X2, X4))
U42_ggaaa(X1, X2, X3, X4, qcF_out_ggggaa(X1, X3, X2, X4, X5)) → mergecC_out_ggaaa(.(X1, X2), .(X3, X4), .(X1, X5))
U43_ggaaa(X1, X2, X3, X4, qcG_out_ggggaa(X1, X3, X2, X4, X5)) → mergecC_out_ggaaa(.(X1, X2), .(X3, X4), .(X3, X5))
qcF_in_ggggaa(X1, X2, [], X3) → U45_ggggaa(X1, X2, X3, lecH_in_gg(X1, X2))
qcF_in_ggggaa(X1, X2, .(X3, X4), X5) → U46_ggggaa(X1, X2, X3, X4, X5, lecH_in_gg(X1, X2))
qcF_in_ggggaa(X1, X2, .(X3, X4), X5) → U48_ggggaa(X1, X2, X3, X4, X5, lecH_in_gg(X1, X2))
qcG_in_ggggaa(X1, X2, X3, []) → U51_ggggaa(X1, X2, X3, gtcI_in_gg(X1, X2))
qcG_in_ggggaa(X1, X2, X3, .(X4, X5)) → U52_ggggaa(X1, X2, X3, X4, X5, gtcI_in_gg(X1, X2))
qcG_in_ggggaa(X1, X2, X3, .(X4, X5)) → U54_ggggaa(X1, X2, X3, X4, X5, gtcI_in_gg(X1, X2))
U45_ggggaa(X1, X2, X3, lecH_out_gg(X1, X2)) → qcF_out_ggggaa(X1, X2, [], X3, .(X2, X3))
U46_ggggaa(X1, X2, X3, X4, X5, lecH_out_gg(X1, X2)) → U47_ggggaa(X1, X2, X3, X4, X5, qcF_in_ggggaa(X3, X2, X4, X5))
U48_ggggaa(X1, X2, X3, X4, X5, lecH_out_gg(X1, X2)) → U49_ggggaa(X1, X2, X3, X4, X5, qcG_in_ggggaa(X3, X2, X4, X5))
U51_ggggaa(X1, X2, X3, gtcI_out_gg(X1, X2)) → qcG_out_ggggaa(X1, X2, X3, [], .(X1, X3))
U52_ggggaa(X1, X2, X3, X4, X5, gtcI_out_gg(X1, X2)) → U53_ggggaa(X1, X2, X3, X4, X5, qcF_in_ggggaa(X1, X4, X3, X5))
U54_ggggaa(X1, X2, X3, X4, X5, gtcI_out_gg(X1, X2)) → U55_ggggaa(X1, X2, X3, X4, X5, qcG_in_ggggaa(X1, X4, X3, X5))
lecH_in_gg(s(X1), s(X2)) → U44_gg(X1, X2, lecH_in_gg(X1, X2))
lecH_in_gg(0, s(0)) → lecH_out_gg(0, s(0))
lecH_in_gg(0, 0) → lecH_out_gg(0, 0)
U47_ggggaa(X1, X2, X3, X4, X5, qcF_out_ggggaa(X3, X2, X4, X5, X6)) → qcF_out_ggggaa(X1, X2, .(X3, X4), X5, .(X3, X6))
U49_ggggaa(X1, X2, X3, X4, X5, qcG_out_ggggaa(X3, X2, X4, X5, X6)) → qcF_out_ggggaa(X1, X2, .(X3, X4), X5, .(X2, X6))
gtcI_in_gg(s(X1), s(X2)) → U50_gg(X1, X2, gtcI_in_gg(X1, X2))
gtcI_in_gg(s(0), 0) → gtcI_out_gg(s(0), 0)
U53_ggggaa(X1, X2, X3, X4, X5, qcF_out_ggggaa(X1, X4, X3, X5, X6)) → qcG_out_ggggaa(X1, X2, X3, .(X4, X5), .(X1, X6))
U55_ggggaa(X1, X2, X3, X4, X5, qcG_out_ggggaa(X1, X4, X3, X5, X6)) → qcG_out_ggggaa(X1, X2, X3, .(X4, X5), .(X4, X6))
U44_gg(X1, X2, lecH_out_gg(X1, X2)) → lecH_out_gg(s(X1), s(X2))
U50_gg(X1, X2, gtcI_out_gg(X1, X2)) → gtcI_out_gg(s(X1), s(X2))
splitcD_in_ggaaa(x0, x1)
mergesortcE_in_gaa(x0)
U37_ggaaa(x0, x1, x2)
U38_gaa(x0, x1, x2, x3)
splitcA_in_gaaa(x0)
U39_gaa(x0, x1, x2, x3, x4)
U32_gaaa(x0, x1, x2)
U40_gaa(x0, x1, x2, x3, x4)
U41_gaa(x0, x1, x2, x3)
mergecC_in_ggaaa(x0, x1)
U42_ggaaa(x0, x1, x2, x3, x4)
U43_ggaaa(x0, x1, x2, x3, x4)
qcF_in_ggggaa(x0, x1, x2, x3)
qcG_in_ggggaa(x0, x1, x2, x3)
U45_ggggaa(x0, x1, x2, x3)
U46_ggggaa(x0, x1, x2, x3, x4, x5)
U48_ggggaa(x0, x1, x2, x3, x4, x5)
U51_ggggaa(x0, x1, x2, x3)
U52_ggggaa(x0, x1, x2, x3, x4, x5)
U54_ggggaa(x0, x1, x2, x3, x4, x5)
lecH_in_gg(x0, x1)
U47_ggggaa(x0, x1, x2, x3, x4, x5)
U49_ggggaa(x0, x1, x2, x3, x4, x5)
gtcI_in_gg(x0, x1)
U53_ggggaa(x0, x1, x2, x3, x4, x5)
U55_ggggaa(x0, x1, x2, x3, x4, x5)
U44_gg(x0, x1, x2)
U50_gg(x0, x1, x2)
MERGESORTE_IN_GAA(.(X1, .(X2, X3))) → U4_GAA(X1, X2, X3, U37_ggaaa(X1, .(X2, X3), U32_gaaa(X2, X3, splitcA_in_gaaa(X3))))
U4_GAA(X1, X2, X3, splitcD_out_ggaaa(X1, .(X2, X3), X7, X8)) → MERGESORTE_IN_GAA(X7)
U4_GAA(X1, X2, X3, splitcD_out_ggaaa(X1, .(X2, X3), X7, X8)) → U6_GAA(X1, X2, X3, X8, mergesortcE_in_gaa(X7))
U6_GAA(X1, X2, X3, X8, mergesortcE_out_gaa(X7, X9)) → MERGESORTE_IN_GAA(X8)
MERGESORTE_IN_GAA(.(X1, .(X2, X3))) → U4_GAA(X1, X2, X3, U37_ggaaa(X1, .(X2, X3), U32_gaaa(X2, X3, splitcA_in_gaaa(X3))))
splitcD_in_ggaaa(X1, X2) → U37_ggaaa(X1, X2, splitcA_in_gaaa(X2))
mergesortcE_in_gaa([]) → mergesortcE_out_gaa([], [])
mergesortcE_in_gaa(.(X1, [])) → mergesortcE_out_gaa(.(X1, []), .(X1, []))
mergesortcE_in_gaa(.(X1, .(X2, X3))) → U38_gaa(X1, X2, X3, splitcD_in_ggaaa(X1, .(X2, X3)))
U37_ggaaa(X1, X2, splitcA_out_gaaa(X2, X4, X3)) → splitcD_out_ggaaa(X1, X2, .(X1, X3), X4)
U38_gaa(X1, X2, X3, splitcD_out_ggaaa(X1, .(X2, X3), X7, X8)) → U39_gaa(X1, X2, X3, X8, mergesortcE_in_gaa(X7))
splitcA_in_gaaa([]) → splitcA_out_gaaa([], [], [])
splitcA_in_gaaa(.(X1, X2)) → U32_gaaa(X1, X2, splitcA_in_gaaa(X2))
U39_gaa(X1, X2, X3, X8, mergesortcE_out_gaa(X7, X9)) → U40_gaa(X1, X2, X3, X9, mergesortcE_in_gaa(X8))
U32_gaaa(X1, X2, splitcA_out_gaaa(X2, X4, X3)) → splitcA_out_gaaa(.(X1, X2), .(X1, X3), X4)
U40_gaa(X1, X2, X3, X9, mergesortcE_out_gaa(X8, X10)) → U41_gaa(X1, X2, X3, mergecC_in_ggaaa(X9, X10))
U41_gaa(X1, X2, X3, mergecC_out_ggaaa(X9, X10, X4)) → mergesortcE_out_gaa(.(X1, .(X2, X3)), X4)
mergecC_in_ggaaa([], X1) → mergecC_out_ggaaa([], X1, X1)
mergecC_in_ggaaa(X1, []) → mergecC_out_ggaaa(X1, [], X1)
mergecC_in_ggaaa(.(X1, X2), .(X3, X4)) → U42_ggaaa(X1, X2, X3, X4, qcF_in_ggggaa(X1, X3, X2, X4))
mergecC_in_ggaaa(.(X1, X2), .(X3, X4)) → U43_ggaaa(X1, X2, X3, X4, qcG_in_ggggaa(X1, X3, X2, X4))
U42_ggaaa(X1, X2, X3, X4, qcF_out_ggggaa(X1, X3, X2, X4, X5)) → mergecC_out_ggaaa(.(X1, X2), .(X3, X4), .(X1, X5))
U43_ggaaa(X1, X2, X3, X4, qcG_out_ggggaa(X1, X3, X2, X4, X5)) → mergecC_out_ggaaa(.(X1, X2), .(X3, X4), .(X3, X5))
qcF_in_ggggaa(X1, X2, [], X3) → U45_ggggaa(X1, X2, X3, lecH_in_gg(X1, X2))
qcF_in_ggggaa(X1, X2, .(X3, X4), X5) → U46_ggggaa(X1, X2, X3, X4, X5, lecH_in_gg(X1, X2))
qcF_in_ggggaa(X1, X2, .(X3, X4), X5) → U48_ggggaa(X1, X2, X3, X4, X5, lecH_in_gg(X1, X2))
qcG_in_ggggaa(X1, X2, X3, []) → U51_ggggaa(X1, X2, X3, gtcI_in_gg(X1, X2))
qcG_in_ggggaa(X1, X2, X3, .(X4, X5)) → U52_ggggaa(X1, X2, X3, X4, X5, gtcI_in_gg(X1, X2))
qcG_in_ggggaa(X1, X2, X3, .(X4, X5)) → U54_ggggaa(X1, X2, X3, X4, X5, gtcI_in_gg(X1, X2))
U45_ggggaa(X1, X2, X3, lecH_out_gg(X1, X2)) → qcF_out_ggggaa(X1, X2, [], X3, .(X2, X3))
U46_ggggaa(X1, X2, X3, X4, X5, lecH_out_gg(X1, X2)) → U47_ggggaa(X1, X2, X3, X4, X5, qcF_in_ggggaa(X3, X2, X4, X5))
U48_ggggaa(X1, X2, X3, X4, X5, lecH_out_gg(X1, X2)) → U49_ggggaa(X1, X2, X3, X4, X5, qcG_in_ggggaa(X3, X2, X4, X5))
U51_ggggaa(X1, X2, X3, gtcI_out_gg(X1, X2)) → qcG_out_ggggaa(X1, X2, X3, [], .(X1, X3))
U52_ggggaa(X1, X2, X3, X4, X5, gtcI_out_gg(X1, X2)) → U53_ggggaa(X1, X2, X3, X4, X5, qcF_in_ggggaa(X1, X4, X3, X5))
U54_ggggaa(X1, X2, X3, X4, X5, gtcI_out_gg(X1, X2)) → U55_ggggaa(X1, X2, X3, X4, X5, qcG_in_ggggaa(X1, X4, X3, X5))
lecH_in_gg(s(X1), s(X2)) → U44_gg(X1, X2, lecH_in_gg(X1, X2))
lecH_in_gg(0, s(0)) → lecH_out_gg(0, s(0))
lecH_in_gg(0, 0) → lecH_out_gg(0, 0)
U47_ggggaa(X1, X2, X3, X4, X5, qcF_out_ggggaa(X3, X2, X4, X5, X6)) → qcF_out_ggggaa(X1, X2, .(X3, X4), X5, .(X3, X6))
U49_ggggaa(X1, X2, X3, X4, X5, qcG_out_ggggaa(X3, X2, X4, X5, X6)) → qcF_out_ggggaa(X1, X2, .(X3, X4), X5, .(X2, X6))
gtcI_in_gg(s(X1), s(X2)) → U50_gg(X1, X2, gtcI_in_gg(X1, X2))
gtcI_in_gg(s(0), 0) → gtcI_out_gg(s(0), 0)
U53_ggggaa(X1, X2, X3, X4, X5, qcF_out_ggggaa(X1, X4, X3, X5, X6)) → qcG_out_ggggaa(X1, X2, X3, .(X4, X5), .(X1, X6))
U55_ggggaa(X1, X2, X3, X4, X5, qcG_out_ggggaa(X1, X4, X3, X5, X6)) → qcG_out_ggggaa(X1, X2, X3, .(X4, X5), .(X4, X6))
U44_gg(X1, X2, lecH_out_gg(X1, X2)) → lecH_out_gg(s(X1), s(X2))
U50_gg(X1, X2, gtcI_out_gg(X1, X2)) → gtcI_out_gg(s(X1), s(X2))
splitcD_in_ggaaa(x0, x1)
mergesortcE_in_gaa(x0)
U37_ggaaa(x0, x1, x2)
U38_gaa(x0, x1, x2, x3)
splitcA_in_gaaa(x0)
U39_gaa(x0, x1, x2, x3, x4)
U32_gaaa(x0, x1, x2)
U40_gaa(x0, x1, x2, x3, x4)
U41_gaa(x0, x1, x2, x3)
mergecC_in_ggaaa(x0, x1)
U42_ggaaa(x0, x1, x2, x3, x4)
U43_ggaaa(x0, x1, x2, x3, x4)
qcF_in_ggggaa(x0, x1, x2, x3)
qcG_in_ggggaa(x0, x1, x2, x3)
U45_ggggaa(x0, x1, x2, x3)
U46_ggggaa(x0, x1, x2, x3, x4, x5)
U48_ggggaa(x0, x1, x2, x3, x4, x5)
U51_ggggaa(x0, x1, x2, x3)
U52_ggggaa(x0, x1, x2, x3, x4, x5)
U54_ggggaa(x0, x1, x2, x3, x4, x5)
lecH_in_gg(x0, x1)
U47_ggggaa(x0, x1, x2, x3, x4, x5)
U49_ggggaa(x0, x1, x2, x3, x4, x5)
gtcI_in_gg(x0, x1)
U53_ggggaa(x0, x1, x2, x3, x4, x5)
U55_ggggaa(x0, x1, x2, x3, x4, x5)
U44_gg(x0, x1, x2)
U50_gg(x0, x1, x2)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
U4_GAA(X1, X2, X3, splitcD_out_ggaaa(X1, .(X2, X3), X7, X8)) → MERGESORTE_IN_GAA(X7)
U4_GAA(X1, X2, X3, splitcD_out_ggaaa(X1, .(X2, X3), X7, X8)) → U6_GAA(X1, X2, X3, X8, mergesortcE_in_gaa(X7))
MERGESORTE_IN_GAA(.(X1, .(X2, X3))) → U4_GAA(X1, X2, X3, U37_ggaaa(X1, .(X2, X3), U32_gaaa(X2, X3, splitcA_in_gaaa(X3))))
POL( U6_GAA(x1, ..., x5) ) = 2x4 + 2x5 + 1
POL( mergesortcE_in_gaa(x1) ) = x1
POL( [] ) = 0
POL( mergesortcE_out_gaa(x1, x2) ) = max{0, -2}
POL( .(x1, x2) ) = 2x2 + 2
POL( U38_gaa(x1, ..., x4) ) = 2x3 + 2
POL( splitcD_in_ggaaa(x1, x2) ) = max{0, 2x1 - 2}
POL( U32_gaaa(x1, ..., x3) ) = 2x3 + 2
POL( U37_ggaaa(x1, ..., x3) ) = x3 + 2
POL( U4_GAA(x1, ..., x4) ) = 2x4 + 2
POL( splitcA_in_gaaa(x1) ) = x1
POL( splitcA_out_gaaa(x1, ..., x3) ) = x2 + 2x3
POL( splitcD_out_ggaaa(x1, ..., x4) ) = x3 + x4
POL( U39_gaa(x1, ..., x5) ) = x3 + 1
POL( U40_gaa(x1, ..., x5) ) = 1
POL( U41_gaa(x1, ..., x4) ) = max{0, -1}
POL( mergecC_in_ggaaa(x1, x2) ) = 1
POL( mergecC_out_ggaaa(x1, ..., x3) ) = x1 + 2x2
POL( U42_ggaaa(x1, ..., x5) ) = max{0, x3 + x4 + x5 - 2}
POL( qcF_in_ggggaa(x1, ..., x4) ) = x2 + x3 + 1
POL( U43_ggaaa(x1, ..., x5) ) = max{0, 2x1 + 2x3 + x4 - 2}
POL( qcG_in_ggggaa(x1, ..., x4) ) = 2x1 + 2x2 + 1
POL( U47_ggggaa(x1, ..., x6) ) = x2 + x3 + 1
POL( U53_ggggaa(x1, ..., x6) ) = max{0, 2x2 + x4 + 2x5 - 2}
POL( U45_ggggaa(x1, ..., x4) ) = x1 + 2x2 + 2
POL( lecH_in_gg(x1, x2) ) = 2
POL( U46_ggggaa(x1, ..., x6) ) = x1 + x4 + 2x5 + x6 + 2
POL( U48_ggggaa(x1, ..., x6) ) = max{0, x1 + x3 + x4 - 2}
POL( qcF_out_ggggaa(x1, ..., x5) ) = max{0, x1 + x4 - 1}
POL( U49_ggggaa(x1, ..., x6) ) = max{0, 2x2 + x5 - 1}
POL( U55_ggggaa(x1, ..., x6) ) = x1 + 2x2 + x3 + 2x4 + 2x5 + 2x6 + 2
POL( U51_ggggaa(x1, ..., x4) ) = x1 + 2x2 + x3 + 2
POL( gtcI_in_gg(x1, x2) ) = 2
POL( U52_ggggaa(x1, ..., x6) ) = max{0, 2x1 + x2 + x3 + 2x4 + 2x5 + 2x6 - 2}
POL( U54_ggggaa(x1, ..., x6) ) = max{0, x6 - 1}
POL( qcG_out_ggggaa(x1, ..., x5) ) = x2 + 2x5 + 2
POL( s(x1) ) = max{0, 2x1 - 2}
POL( U44_gg(x1, ..., x3) ) = x1 + x2 + 2x3 + 2
POL( 0 ) = 0
POL( lecH_out_gg(x1, x2) ) = max{0, x1 - 1}
POL( U50_gg(x1, ..., x3) ) = x1 + 2
POL( gtcI_out_gg(x1, x2) ) = 0
POL( MERGESORTE_IN_GAA(x1) ) = 2x1 + 1
mergesortcE_in_gaa([]) → mergesortcE_out_gaa([], [])
mergesortcE_in_gaa(.(X1, [])) → mergesortcE_out_gaa(.(X1, []), .(X1, []))
mergesortcE_in_gaa(.(X1, .(X2, X3))) → U38_gaa(X1, X2, X3, splitcD_in_ggaaa(X1, .(X2, X3)))
splitcA_in_gaaa([]) → splitcA_out_gaaa([], [], [])
splitcA_in_gaaa(.(X1, X2)) → U32_gaaa(X1, X2, splitcA_in_gaaa(X2))
U32_gaaa(X1, X2, splitcA_out_gaaa(X2, X4, X3)) → splitcA_out_gaaa(.(X1, X2), .(X1, X3), X4)
U37_ggaaa(X1, X2, splitcA_out_gaaa(X2, X4, X3)) → splitcD_out_ggaaa(X1, X2, .(X1, X3), X4)
U38_gaa(X1, X2, X3, splitcD_out_ggaaa(X1, .(X2, X3), X7, X8)) → U39_gaa(X1, X2, X3, X8, mergesortcE_in_gaa(X7))
U39_gaa(X1, X2, X3, X8, mergesortcE_out_gaa(X7, X9)) → U40_gaa(X1, X2, X3, X9, mergesortcE_in_gaa(X8))
U40_gaa(X1, X2, X3, X9, mergesortcE_out_gaa(X8, X10)) → U41_gaa(X1, X2, X3, mergecC_in_ggaaa(X9, X10))
U41_gaa(X1, X2, X3, mergecC_out_ggaaa(X9, X10, X4)) → mergesortcE_out_gaa(.(X1, .(X2, X3)), X4)
U6_GAA(X1, X2, X3, X8, mergesortcE_out_gaa(X7, X9)) → MERGESORTE_IN_GAA(X8)
splitcD_in_ggaaa(X1, X2) → U37_ggaaa(X1, X2, splitcA_in_gaaa(X2))
mergesortcE_in_gaa([]) → mergesortcE_out_gaa([], [])
mergesortcE_in_gaa(.(X1, [])) → mergesortcE_out_gaa(.(X1, []), .(X1, []))
mergesortcE_in_gaa(.(X1, .(X2, X3))) → U38_gaa(X1, X2, X3, splitcD_in_ggaaa(X1, .(X2, X3)))
U37_ggaaa(X1, X2, splitcA_out_gaaa(X2, X4, X3)) → splitcD_out_ggaaa(X1, X2, .(X1, X3), X4)
U38_gaa(X1, X2, X3, splitcD_out_ggaaa(X1, .(X2, X3), X7, X8)) → U39_gaa(X1, X2, X3, X8, mergesortcE_in_gaa(X7))
splitcA_in_gaaa([]) → splitcA_out_gaaa([], [], [])
splitcA_in_gaaa(.(X1, X2)) → U32_gaaa(X1, X2, splitcA_in_gaaa(X2))
U39_gaa(X1, X2, X3, X8, mergesortcE_out_gaa(X7, X9)) → U40_gaa(X1, X2, X3, X9, mergesortcE_in_gaa(X8))
U32_gaaa(X1, X2, splitcA_out_gaaa(X2, X4, X3)) → splitcA_out_gaaa(.(X1, X2), .(X1, X3), X4)
U40_gaa(X1, X2, X3, X9, mergesortcE_out_gaa(X8, X10)) → U41_gaa(X1, X2, X3, mergecC_in_ggaaa(X9, X10))
U41_gaa(X1, X2, X3, mergecC_out_ggaaa(X9, X10, X4)) → mergesortcE_out_gaa(.(X1, .(X2, X3)), X4)
mergecC_in_ggaaa([], X1) → mergecC_out_ggaaa([], X1, X1)
mergecC_in_ggaaa(X1, []) → mergecC_out_ggaaa(X1, [], X1)
mergecC_in_ggaaa(.(X1, X2), .(X3, X4)) → U42_ggaaa(X1, X2, X3, X4, qcF_in_ggggaa(X1, X3, X2, X4))
mergecC_in_ggaaa(.(X1, X2), .(X3, X4)) → U43_ggaaa(X1, X2, X3, X4, qcG_in_ggggaa(X1, X3, X2, X4))
U42_ggaaa(X1, X2, X3, X4, qcF_out_ggggaa(X1, X3, X2, X4, X5)) → mergecC_out_ggaaa(.(X1, X2), .(X3, X4), .(X1, X5))
U43_ggaaa(X1, X2, X3, X4, qcG_out_ggggaa(X1, X3, X2, X4, X5)) → mergecC_out_ggaaa(.(X1, X2), .(X3, X4), .(X3, X5))
qcF_in_ggggaa(X1, X2, [], X3) → U45_ggggaa(X1, X2, X3, lecH_in_gg(X1, X2))
qcF_in_ggggaa(X1, X2, .(X3, X4), X5) → U46_ggggaa(X1, X2, X3, X4, X5, lecH_in_gg(X1, X2))
qcF_in_ggggaa(X1, X2, .(X3, X4), X5) → U48_ggggaa(X1, X2, X3, X4, X5, lecH_in_gg(X1, X2))
qcG_in_ggggaa(X1, X2, X3, []) → U51_ggggaa(X1, X2, X3, gtcI_in_gg(X1, X2))
qcG_in_ggggaa(X1, X2, X3, .(X4, X5)) → U52_ggggaa(X1, X2, X3, X4, X5, gtcI_in_gg(X1, X2))
qcG_in_ggggaa(X1, X2, X3, .(X4, X5)) → U54_ggggaa(X1, X2, X3, X4, X5, gtcI_in_gg(X1, X2))
U45_ggggaa(X1, X2, X3, lecH_out_gg(X1, X2)) → qcF_out_ggggaa(X1, X2, [], X3, .(X2, X3))
U46_ggggaa(X1, X2, X3, X4, X5, lecH_out_gg(X1, X2)) → U47_ggggaa(X1, X2, X3, X4, X5, qcF_in_ggggaa(X3, X2, X4, X5))
U48_ggggaa(X1, X2, X3, X4, X5, lecH_out_gg(X1, X2)) → U49_ggggaa(X1, X2, X3, X4, X5, qcG_in_ggggaa(X3, X2, X4, X5))
U51_ggggaa(X1, X2, X3, gtcI_out_gg(X1, X2)) → qcG_out_ggggaa(X1, X2, X3, [], .(X1, X3))
U52_ggggaa(X1, X2, X3, X4, X5, gtcI_out_gg(X1, X2)) → U53_ggggaa(X1, X2, X3, X4, X5, qcF_in_ggggaa(X1, X4, X3, X5))
U54_ggggaa(X1, X2, X3, X4, X5, gtcI_out_gg(X1, X2)) → U55_ggggaa(X1, X2, X3, X4, X5, qcG_in_ggggaa(X1, X4, X3, X5))
lecH_in_gg(s(X1), s(X2)) → U44_gg(X1, X2, lecH_in_gg(X1, X2))
lecH_in_gg(0, s(0)) → lecH_out_gg(0, s(0))
lecH_in_gg(0, 0) → lecH_out_gg(0, 0)
U47_ggggaa(X1, X2, X3, X4, X5, qcF_out_ggggaa(X3, X2, X4, X5, X6)) → qcF_out_ggggaa(X1, X2, .(X3, X4), X5, .(X3, X6))
U49_ggggaa(X1, X2, X3, X4, X5, qcG_out_ggggaa(X3, X2, X4, X5, X6)) → qcF_out_ggggaa(X1, X2, .(X3, X4), X5, .(X2, X6))
gtcI_in_gg(s(X1), s(X2)) → U50_gg(X1, X2, gtcI_in_gg(X1, X2))
gtcI_in_gg(s(0), 0) → gtcI_out_gg(s(0), 0)
U53_ggggaa(X1, X2, X3, X4, X5, qcF_out_ggggaa(X1, X4, X3, X5, X6)) → qcG_out_ggggaa(X1, X2, X3, .(X4, X5), .(X1, X6))
U55_ggggaa(X1, X2, X3, X4, X5, qcG_out_ggggaa(X1, X4, X3, X5, X6)) → qcG_out_ggggaa(X1, X2, X3, .(X4, X5), .(X4, X6))
U44_gg(X1, X2, lecH_out_gg(X1, X2)) → lecH_out_gg(s(X1), s(X2))
U50_gg(X1, X2, gtcI_out_gg(X1, X2)) → gtcI_out_gg(s(X1), s(X2))
splitcD_in_ggaaa(x0, x1)
mergesortcE_in_gaa(x0)
U37_ggaaa(x0, x1, x2)
U38_gaa(x0, x1, x2, x3)
splitcA_in_gaaa(x0)
U39_gaa(x0, x1, x2, x3, x4)
U32_gaaa(x0, x1, x2)
U40_gaa(x0, x1, x2, x3, x4)
U41_gaa(x0, x1, x2, x3)
mergecC_in_ggaaa(x0, x1)
U42_ggaaa(x0, x1, x2, x3, x4)
U43_ggaaa(x0, x1, x2, x3, x4)
qcF_in_ggggaa(x0, x1, x2, x3)
qcG_in_ggggaa(x0, x1, x2, x3)
U45_ggggaa(x0, x1, x2, x3)
U46_ggggaa(x0, x1, x2, x3, x4, x5)
U48_ggggaa(x0, x1, x2, x3, x4, x5)
U51_ggggaa(x0, x1, x2, x3)
U52_ggggaa(x0, x1, x2, x3, x4, x5)
U54_ggggaa(x0, x1, x2, x3, x4, x5)
lecH_in_gg(x0, x1)
U47_ggggaa(x0, x1, x2, x3, x4, x5)
U49_ggggaa(x0, x1, x2, x3, x4, x5)
gtcI_in_gg(x0, x1)
U53_ggggaa(x0, x1, x2, x3, x4, x5)
U55_ggggaa(x0, x1, x2, x3, x4, x5)
U44_gg(x0, x1, x2)
U50_gg(x0, x1, x2)
MERGESORTB_IN_GAA(.(X1, .(X2, X3)), X4, .(X5, X6)) → U25_GAA(X1, X2, X3, X4, X5, X6, splitcD_in_ggaaa(X2, X3, X7, X8, X6))
U25_GAA(X1, X2, X3, X4, X5, X6, splitcD_out_ggaaa(X2, X3, X7, X8, X6)) → MERGESORTB_IN_GAA(.(X1, X8), X9, X6)
splitcD_in_ggaaa(X1, X2, .(X1, X3), X4, .(X5, X6)) → U37_ggaaa(X1, X2, X3, X4, X5, X6, splitcA_in_gaaa(X2, X4, X3, X6))
splitcA_in_gaaa([], [], [], X1) → splitcA_out_gaaa([], [], [], X1)
splitcA_in_gaaa(.(X1, X2), .(X1, X3), X4, .(X5, X6)) → U32_gaaa(X1, X2, X3, X4, X5, X6, splitcA_in_gaaa(X2, X4, X3, X6))
U32_gaaa(X1, X2, X3, X4, X5, X6, splitcA_out_gaaa(X2, X4, X3, X6)) → splitcA_out_gaaa(.(X1, X2), .(X1, X3), X4, .(X5, X6))
U37_ggaaa(X1, X2, X3, X4, X5, X6, splitcA_out_gaaa(X2, X4, X3, X6)) → splitcD_out_ggaaa(X1, X2, .(X1, X3), X4, .(X5, X6))
mergesortcB_in_gaa([], [], X1) → mergesortcB_out_gaa([], [], X1)
mergesortcB_in_gaa(.(X1, []), .(X1, []), X2) → mergesortcB_out_gaa(.(X1, []), .(X1, []), X2)
mergesortcB_in_gaa(.(X1, .(X2, X3)), X4, .(X5, X6)) → U33_gaa(X1, X2, X3, X4, X5, X6, splitcD_in_ggaaa(X2, X3, X7, X8, X6))
U33_gaa(X1, X2, X3, X4, X5, X6, splitcD_out_ggaaa(X2, X3, X7, X8, X6)) → U34_gaa(X1, X2, X3, X4, X5, X6, X7, mergesortcB_in_gaa(.(X1, X8), X9, X6))
U34_gaa(X1, X2, X3, X4, X5, X6, X7, mergesortcB_out_gaa(.(X1, X8), X9, X6)) → U35_gaa(X1, X2, X3, X4, X5, X6, X9, mergesortcE_in_gaa(X7, X10, X6))
mergesortcE_in_gaa([], [], X1) → mergesortcE_out_gaa([], [], X1)
mergesortcE_in_gaa(.(X1, []), .(X1, []), X2) → mergesortcE_out_gaa(.(X1, []), .(X1, []), X2)
mergesortcE_in_gaa(.(X1, .(X2, X3)), X4, .(X5, X6)) → U38_gaa(X1, X2, X3, X4, X5, X6, splitcD_in_ggaaa(X1, .(X2, X3), X7, X8, .(X5, X6)))
U38_gaa(X1, X2, X3, X4, X5, X6, splitcD_out_ggaaa(X1, .(X2, X3), X7, X8, .(X5, X6))) → U39_gaa(X1, X2, X3, X4, X5, X6, X8, mergesortcE_in_gaa(X7, X9, X6))
U39_gaa(X1, X2, X3, X4, X5, X6, X8, mergesortcE_out_gaa(X7, X9, X6)) → U40_gaa(X1, X2, X3, X4, X5, X6, X9, mergesortcE_in_gaa(X8, X10, X6))
U40_gaa(X1, X2, X3, X4, X5, X6, X9, mergesortcE_out_gaa(X8, X10, X6)) → U41_gaa(X1, X2, X3, X4, X5, X6, mergecC_in_ggaaa(X9, X10, X4, X5, X6))
mergecC_in_ggaaa([], X1, X1, X2, X3) → mergecC_out_ggaaa([], X1, X1, X2, X3)
mergecC_in_ggaaa(X1, [], X1, X2, X3) → mergecC_out_ggaaa(X1, [], X1, X2, X3)
mergecC_in_ggaaa(.(X1, X2), .(X3, X4), .(X1, X5), X6, X7) → U42_ggaaa(X1, X2, X3, X4, X5, X6, X7, qcF_in_ggggaa(X1, X3, X2, X4, X5, X7))
qcF_in_ggggaa(X1, X2, [], X3, .(X2, X3), X4) → U45_ggggaa(X1, X2, X3, X4, lecH_in_gg(X1, X2))
lecH_in_gg(s(X1), s(X2)) → U44_gg(X1, X2, lecH_in_gg(X1, X2))
lecH_in_gg(0, s(0)) → lecH_out_gg(0, s(0))
lecH_in_gg(0, 0) → lecH_out_gg(0, 0)
U44_gg(X1, X2, lecH_out_gg(X1, X2)) → lecH_out_gg(s(X1), s(X2))
U45_ggggaa(X1, X2, X3, X4, lecH_out_gg(X1, X2)) → qcF_out_ggggaa(X1, X2, [], X3, .(X2, X3), X4)
qcF_in_ggggaa(X1, X2, .(X3, X4), X5, .(X3, X6), .(X7, X8)) → U46_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, lecH_in_gg(X1, X2))
U46_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, lecH_out_gg(X1, X2)) → U47_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, qcF_in_ggggaa(X3, X2, X4, X5, X6, X8))
qcF_in_ggggaa(X1, X2, .(X3, X4), X5, .(X2, X6), .(X7, X8)) → U48_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, lecH_in_gg(X1, X2))
U48_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, lecH_out_gg(X1, X2)) → U49_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, qcG_in_ggggaa(X3, X2, X4, X5, X6, X8))
qcG_in_ggggaa(X1, X2, X3, [], .(X1, X3), X4) → U51_ggggaa(X1, X2, X3, X4, gtcI_in_gg(X1, X2))
gtcI_in_gg(s(X1), s(X2)) → U50_gg(X1, X2, gtcI_in_gg(X1, X2))
gtcI_in_gg(s(0), 0) → gtcI_out_gg(s(0), 0)
U50_gg(X1, X2, gtcI_out_gg(X1, X2)) → gtcI_out_gg(s(X1), s(X2))
U51_ggggaa(X1, X2, X3, X4, gtcI_out_gg(X1, X2)) → qcG_out_ggggaa(X1, X2, X3, [], .(X1, X3), X4)
qcG_in_ggggaa(X1, X2, X3, .(X4, X5), .(X1, X6), .(X7, X8)) → U52_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, gtcI_in_gg(X1, X2))
U52_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, gtcI_out_gg(X1, X2)) → U53_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, qcF_in_ggggaa(X1, X4, X3, X5, X6, X8))
U53_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, qcF_out_ggggaa(X1, X4, X3, X5, X6, X8)) → qcG_out_ggggaa(X1, X2, X3, .(X4, X5), .(X1, X6), .(X7, X8))
qcG_in_ggggaa(X1, X2, X3, .(X4, X5), .(X4, X6), .(X7, X8)) → U54_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, gtcI_in_gg(X1, X2))
U54_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, gtcI_out_gg(X1, X2)) → U55_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, qcG_in_ggggaa(X1, X4, X3, X5, X6, X8))
U55_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, qcG_out_ggggaa(X1, X4, X3, X5, X6, X8)) → qcG_out_ggggaa(X1, X2, X3, .(X4, X5), .(X4, X6), .(X7, X8))
U49_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, qcG_out_ggggaa(X3, X2, X4, X5, X6, X8)) → qcF_out_ggggaa(X1, X2, .(X3, X4), X5, .(X2, X6), .(X7, X8))
U47_ggggaa(X1, X2, X3, X4, X5, X6, X7, X8, qcF_out_ggggaa(X3, X2, X4, X5, X6, X8)) → qcF_out_ggggaa(X1, X2, .(X3, X4), X5, .(X3, X6), .(X7, X8))
U42_ggaaa(X1, X2, X3, X4, X5, X6, X7, qcF_out_ggggaa(X1, X3, X2, X4, X5, X7)) → mergecC_out_ggaaa(.(X1, X2), .(X3, X4), .(X1, X5), X6, X7)
mergecC_in_ggaaa(.(X1, X2), .(X3, X4), .(X3, X5), X6, X7) → U43_ggaaa(X1, X2, X3, X4, X5, X6, X7, qcG_in_ggggaa(X1, X3, X2, X4, X5, X7))
U43_ggaaa(X1, X2, X3, X4, X5, X6, X7, qcG_out_ggggaa(X1, X3, X2, X4, X5, X7)) → mergecC_out_ggaaa(.(X1, X2), .(X3, X4), .(X3, X5), X6, X7)
U41_gaa(X1, X2, X3, X4, X5, X6, mergecC_out_ggaaa(X9, X10, X4, X5, X6)) → mergesortcE_out_gaa(.(X1, .(X2, X3)), X4, .(X5, X6))
U35_gaa(X1, X2, X3, X4, X5, X6, X9, mergesortcE_out_gaa(X7, X10, X6)) → U36_gaa(X1, X2, X3, X4, X5, X6, mergecC_in_ggaaa(X9, X10, X4, X5, X6))
U36_gaa(X1, X2, X3, X4, X5, X6, mergecC_out_ggaaa(X9, X10, X4, X5, X6)) → mergesortcB_out_gaa(.(X1, .(X2, X3)), X4, .(X5, X6))
MERGESORTB_IN_GAA(.(X1, .(X2, X3)), X4, .(X5, X6)) → U25_GAA(X1, X2, X3, X4, X5, X6, splitcD_in_ggaaa(X2, X3, X7, X8, X6))
U25_GAA(X1, X2, X3, X4, X5, X6, splitcD_out_ggaaa(X2, X3, X7, X8, X6)) → MERGESORTB_IN_GAA(.(X1, X8), X9, X6)
splitcD_in_ggaaa(X1, X2, .(X1, X3), X4, .(X5, X6)) → U37_ggaaa(X1, X2, X3, X4, X5, X6, splitcA_in_gaaa(X2, X4, X3, X6))
U37_ggaaa(X1, X2, X3, X4, X5, X6, splitcA_out_gaaa(X2, X4, X3, X6)) → splitcD_out_ggaaa(X1, X2, .(X1, X3), X4, .(X5, X6))
splitcA_in_gaaa([], [], [], X1) → splitcA_out_gaaa([], [], [], X1)
splitcA_in_gaaa(.(X1, X2), .(X1, X3), X4, .(X5, X6)) → U32_gaaa(X1, X2, X3, X4, X5, X6, splitcA_in_gaaa(X2, X4, X3, X6))
U32_gaaa(X1, X2, X3, X4, X5, X6, splitcA_out_gaaa(X2, X4, X3, X6)) → splitcA_out_gaaa(.(X1, X2), .(X1, X3), X4, .(X5, X6))
MERGESORTB_IN_GAA(.(X1, .(X2, X3))) → U25_GAA(X1, X2, X3, splitcD_in_ggaaa(X2, X3))
U25_GAA(X1, X2, X3, splitcD_out_ggaaa(X2, X3, X7, X8)) → MERGESORTB_IN_GAA(.(X1, X8))
splitcD_in_ggaaa(X1, X2) → U37_ggaaa(X1, X2, splitcA_in_gaaa(X2))
U37_ggaaa(X1, X2, splitcA_out_gaaa(X2, X4, X3)) → splitcD_out_ggaaa(X1, X2, .(X1, X3), X4)
splitcA_in_gaaa([]) → splitcA_out_gaaa([], [], [])
splitcA_in_gaaa(.(X1, X2)) → U32_gaaa(X1, X2, splitcA_in_gaaa(X2))
U32_gaaa(X1, X2, splitcA_out_gaaa(X2, X4, X3)) → splitcA_out_gaaa(.(X1, X2), .(X1, X3), X4)
splitcD_in_ggaaa(x0, x1)
U37_ggaaa(x0, x1, x2)
splitcA_in_gaaa(x0)
U32_gaaa(x0, x1, x2)
MERGESORTB_IN_GAA(.(X1, .(X2, X3))) → U25_GAA(X1, X2, X3, U37_ggaaa(X2, X3, splitcA_in_gaaa(X3)))
U25_GAA(X1, X2, X3, splitcD_out_ggaaa(X2, X3, X7, X8)) → MERGESORTB_IN_GAA(.(X1, X8))
MERGESORTB_IN_GAA(.(X1, .(X2, X3))) → U25_GAA(X1, X2, X3, U37_ggaaa(X2, X3, splitcA_in_gaaa(X3)))
splitcD_in_ggaaa(X1, X2) → U37_ggaaa(X1, X2, splitcA_in_gaaa(X2))
U37_ggaaa(X1, X2, splitcA_out_gaaa(X2, X4, X3)) → splitcD_out_ggaaa(X1, X2, .(X1, X3), X4)
splitcA_in_gaaa([]) → splitcA_out_gaaa([], [], [])
splitcA_in_gaaa(.(X1, X2)) → U32_gaaa(X1, X2, splitcA_in_gaaa(X2))
U32_gaaa(X1, X2, splitcA_out_gaaa(X2, X4, X3)) → splitcA_out_gaaa(.(X1, X2), .(X1, X3), X4)
splitcD_in_ggaaa(x0, x1)
U37_ggaaa(x0, x1, x2)
splitcA_in_gaaa(x0)
U32_gaaa(x0, x1, x2)
U25_GAA(X1, X2, X3, splitcD_out_ggaaa(X2, X3, X7, X8)) → MERGESORTB_IN_GAA(.(X1, X8))
MERGESORTB_IN_GAA(.(X1, .(X2, X3))) → U25_GAA(X1, X2, X3, U37_ggaaa(X2, X3, splitcA_in_gaaa(X3)))
splitcA_in_gaaa([]) → splitcA_out_gaaa([], [], [])
splitcA_in_gaaa(.(X1, X2)) → U32_gaaa(X1, X2, splitcA_in_gaaa(X2))
U37_ggaaa(X1, X2, splitcA_out_gaaa(X2, X4, X3)) → splitcD_out_ggaaa(X1, X2, .(X1, X3), X4)
U32_gaaa(X1, X2, splitcA_out_gaaa(X2, X4, X3)) → splitcA_out_gaaa(.(X1, X2), .(X1, X3), X4)
splitcD_in_ggaaa(x0, x1)
U37_ggaaa(x0, x1, x2)
splitcA_in_gaaa(x0)
U32_gaaa(x0, x1, x2)
splitcD_in_ggaaa(x0, x1)
U25_GAA(X1, X2, X3, splitcD_out_ggaaa(X2, X3, X7, X8)) → MERGESORTB_IN_GAA(.(X1, X8))
MERGESORTB_IN_GAA(.(X1, .(X2, X3))) → U25_GAA(X1, X2, X3, U37_ggaaa(X2, X3, splitcA_in_gaaa(X3)))
splitcA_in_gaaa([]) → splitcA_out_gaaa([], [], [])
splitcA_in_gaaa(.(X1, X2)) → U32_gaaa(X1, X2, splitcA_in_gaaa(X2))
U37_ggaaa(X1, X2, splitcA_out_gaaa(X2, X4, X3)) → splitcD_out_ggaaa(X1, X2, .(X1, X3), X4)
U32_gaaa(X1, X2, splitcA_out_gaaa(X2, X4, X3)) → splitcA_out_gaaa(.(X1, X2), .(X1, X3), X4)
U37_ggaaa(x0, x1, x2)
splitcA_in_gaaa(x0)
U32_gaaa(x0, x1, x2)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
MERGESORTB_IN_GAA(.(X1, .(X2, X3))) → U25_GAA(X1, X2, X3, U37_ggaaa(X2, X3, splitcA_in_gaaa(X3)))
POL(.(x1, x2)) = 1 + x2
POL(MERGESORTB_IN_GAA(x1)) = x1
POL(U25_GAA(x1, x2, x3, x4)) = x4
POL(U32_gaaa(x1, x2, x3)) = 1 + x3
POL(U37_ggaaa(x1, x2, x3)) = 1 + x3
POL([]) = 0
POL(splitcA_in_gaaa(x1)) = x1
POL(splitcA_out_gaaa(x1, x2, x3)) = x2 + x3
POL(splitcD_out_ggaaa(x1, x2, x3, x4)) = 1 + x4
splitcA_in_gaaa([]) → splitcA_out_gaaa([], [], [])
splitcA_in_gaaa(.(X1, X2)) → U32_gaaa(X1, X2, splitcA_in_gaaa(X2))
U37_ggaaa(X1, X2, splitcA_out_gaaa(X2, X4, X3)) → splitcD_out_ggaaa(X1, X2, .(X1, X3), X4)
U32_gaaa(X1, X2, splitcA_out_gaaa(X2, X4, X3)) → splitcA_out_gaaa(.(X1, X2), .(X1, X3), X4)
U25_GAA(X1, X2, X3, splitcD_out_ggaaa(X2, X3, X7, X8)) → MERGESORTB_IN_GAA(.(X1, X8))
splitcA_in_gaaa([]) → splitcA_out_gaaa([], [], [])
splitcA_in_gaaa(.(X1, X2)) → U32_gaaa(X1, X2, splitcA_in_gaaa(X2))
U37_ggaaa(X1, X2, splitcA_out_gaaa(X2, X4, X3)) → splitcD_out_ggaaa(X1, X2, .(X1, X3), X4)
U32_gaaa(X1, X2, splitcA_out_gaaa(X2, X4, X3)) → splitcA_out_gaaa(.(X1, X2), .(X1, X3), X4)
U37_ggaaa(x0, x1, x2)
splitcA_in_gaaa(x0)
U32_gaaa(x0, x1, x2)